20201221-induction-by-reflection-schoisswohl Benchmarks
Family
Name
induction-by-reflection-schoisswohl
Generation Date
2020-12-21
First Occurrence
2021-07-18
Benchmarks
77
Benchmarks
UF
•
Charts
•
Solver Isomap
reflectiveInductive/revAppend-0.smt2
reflectiveInductive/revAppend-1.smt2
reflectiveInductive/addCommutId.smt2
reflectiveInductive/addCommut.smt2
reflectiveInductive/addNeutral-0.smt2
reflectiveInductive/appendMonoton.smt2
reflectiveInductive/addAssoc.smt2
reflectiveInductive/addNeutral-1.smt2
reflectiveInductive/revsEqual.smt2
reflectiveInductive/distr-1.smt2
reflectiveInductive/addNeutral.smt2
reflectiveInductive/zeroMin.smt2
reflectiveInductive/distr-0.smt2
reflectiveInductive/revSelfInvers.smt2
reflectiveInductive/mulCommut.smt2
reflectiveInductive/leqTrans.smt2
reflectiveInductive/mulZero.smt2
reflectiveInductive/appendAssoc.smt2
reflectiveInductive/allEqRefl.smt2
reflectiveInductive/addMonoton-0.smt2
reflectiveInductive/allEqDefsEquality.smt2
reflectiveInductive/mulAssoc.smt2
reflectiveInductive/addMonoton-1.smt2
reflectiveConjecture/currying-0.smt2
reflectiveConjecture/eqRefl.smt2
reflectiveConjecture/contraposition-0.smt2
reflectiveConjecture/universalInstance.smt2
reflectiveConjecture/currying-1.smt2
reflectiveConjecture/eqTrans.smt2
reflectiveConjecture/contraposition-1.smt2
reflectiveConjecture/excludedMiddle-0.smt2
reflectiveConjecture/excludedMiddle-1.smt2
UFDT
•
Charts
•
Solver Isomap
reflectiveAxioms/N+Leq+Add+Mul-ax2.smt2
reflectiveAxioms/N+Leq+Add+Mul-ax3.smt2
reflectiveAxioms/N+Leq+Add+Mul-ax5.smt2
reflectiveAxioms/N+L+Pref+App-ax0.smt2
reflectiveAxioms/N+Leq+Add+Mul-ax0.smt2
reflectiveAxioms/N+Leq+Add+Mul-ax1.smt2
reflectiveAxioms/N+L+Pref+App-ax2.smt2
reflectiveAxioms/N+L+Pref+App-ax4.smt2
reflectiveAxioms/N+L+Pref+App-ax1.smt2
reflectiveAxioms/N+Leq+Add+Mul-ax4.smt2
reflectiveAxioms/N+L+Pref+App-ax3.smt2
reflectiveConjecture/addGround-0.smt2
reflectiveConjecture/existsZeroAdd.smt2
reflectiveConjecture/mulExists.smt2
reflectiveConjecture/addGround-1.smt2
reflectiveConjecture/appendGround-0.smt2
reflectiveConjecture/appendGround-1.smt2
reflectiveConjecture/addExists.smt2
reflectiveConjecture/existsNil.smt2
reflectiveConjecture/appendExists.smt2
reflectiveConjecture/mulGround.smt2
inductive/revAppend-0.smt2
reflectiveConjecture/existsZeroMul.smt2
inductive/revAppend-1.smt2
inductive/addCommut.smt2
inductive/addCommutId.smt2
inductive/appendMonoton.smt2
inductive/addNeutral-0.smt2
inductive/addAssoc.smt2
inductive/revsEqual.smt2
inductive/addNeutral-1.smt2
inductive/distr-1.smt2
inductive/addNeutral.smt2
inductive/zeroMin.smt2
inductive/distr-0.smt2
inductive/revSelfInvers.smt2
inductive/mulCommut.smt2
inductive/leqTrans.smt2
inductive/mulZero.smt2
inductive/appendAssoc.smt2
inductive/allEqRefl.smt2
inductive/addMonoton-0.smt2
inductive/allEqDefsEquality.smt2
inductive/mulAssoc.smt2
inductive/addMonoton-1.smt2