%------------------------------------------------------------------------------ % File : E-Darwin---1.5 % Problem : LCL407-2 : TPTP v6.1.0. Released v2.5.0. % Transfm : none % Format : tptp:raw % Command : e-darwin -pev TPTP -pmd true -if tptp -pl 2 -pc false -ps false %s % Computer : n031.star.cs.uiowa.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz % Memory : 16127.75MB % OS : Linux 2.6.32-431.20.3.el6.x86_64 % CPULimit : 300s % DateTime : Fri Aug 1 22:04:50 EDT 2014 % Result : Satisfiable 0.31s % Output : Model 0.31s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : LCL407-2 : TPTP v6.1.0. Released v2.5.0. % % Command : e-darwin -pev TPTP -pmd true -if tptp -pl 2 -pc false -ps false %s % % Computer : n031.star.cs.uiowa.edu % % Model : x86_64 x86_64 % % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % % Memory : 16127.75MB % % OS : Linux 2.6.32-431.20.3.el6.x86_64 % % CPULimit : 300 % % DateTime : Sat Jul 26 05:19:51 CDT 2014 % % CPUTime : 0.31 % E-Darwin 1.5 2012/06/20 (based on Darwin 1.3) % % % Defaulting to tptp format. % Parsing /export/starexec/sandbox/benchmark/theBenchmark.p ... % Parsing /export/starexec/sandbox/benchmark/Axioms/LCL002-0.ax ... % % % % Proving ... % % % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % % START OF MODEL (DIG): % (xor(_0, xor(falsehood, _1)) = xor(_0, _1)) % (xor(xor(_0, truth), _1) = xor(_0, xor(truth, _1))) % (xor(_0, falsehood) = _0) % (xor(_0, xor(truth, _1)) = xor(not(_0), _1)) % (xor(_0, _0) = falsehood) % (xor(xor(falsehood, _0), _0) = falsehood) % (xor(not(xor(truth, _0)), _0) = falsehood) % (and_star(xor(truth, _0), _0) = falsehood) % (and_star(xor(truth, _0), xor(falsehood, _0)) = falsehood) % (and_star(xor(falsehood, _0), xor(truth, _0)) = falsehood) % (and_star(xor(and_star(xor(truth, _0), _1), truth), _1) = and_star(xor(and_star(xor(truth, _1), _0), truth), _0)) % (and_star(_0, truth) = _0) % (and_star(_0, falsehood) = falsehood) % (and_star(truth, xor(falsehood, _0)) = and_star(truth, _0)) % (and_star(not(truth), truth) = falsehood) % (and_star(not(and_star(xor(truth, _0), _1)), _1) = and_star(not(and_star(xor(truth, _1), _0)), _0)) % (and_star(not(and_star(xor(truth, _1), _0)), _0) = and_star(not(and_star(xor(truth, _0), xor(falsehood, _1))), xor(falsehood, _1))) % (and_star(not(and_star(xor(truth, _0), xor(falsehood, _1))), xor(falsehood, _1)) = and_star(not(and_star(xor(truth, _0), _1)), _1)) % (and_star(not(and_star(xor(truth, _0), xor(falsehood, _1))), xor(falsehood, _1)) = and_star(not(and_star(xor(truth, _1), xor(falsehood, _0))), xor(falsehood, _0))) % (and_star(not(and_star(xor(falsehood, _1), _0)), _0) = and_star(not(and_star(xor(truth, _0), xor(truth, _1))), xor(truth, _1))) % (and_star(not(and_star(xor(falsehood, _0), xor(falsehood, _1))), xor(falsehood, _1)) = and_star(not(and_star(xor(falsehood, _0), _1)), _1)) % (and_star(not(and_star(xor(falsehood, _0), xor(truth, _1))), xor(truth, _1)) = and_star(not(and_star(xor(falsehood, _1), xor(truth, _0))), xor(truth, _0))) % (and_star(not(and_star(xor(falsehood, _1), xor(falsehood, _0))), xor(falsehood, _0)) = and_star(not(and_star(xor(truth, _0), xor(truth, _1))), xor(truth, _1))) % (and_star(not(and_star(truth, _0)), _0) = falsehood) % (and_star(not(and_star(truth, _0)), xor(falsehood, _0)) = falsehood) % (and_star(not(and_star(not(truth), _0)), _0) = and_star(not(and_star(xor(truth, _0), truth)), truth)) % (and_star(not(and_star(falsehood, _0)), _0) = not(xor(truth, _0))) % (xor(_0, truth) = not(_0)) % (not(truth) = falsehood) % (not(falsehood) = truth) % (xor(_0, not(truth)) = not(not(_0))) % (not(not(_0)) = _0) % true % END OF MODEL % EOF %------------------------------------------------------------------------------