%------------------------------------------------------------------------------ % File : E-Darwin---1.5 % Problem : SYN720-1 : 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 : n021.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:18:12 EDT 2014 % Result : Satisfiable 0.33s % Output : Model 0.33s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : SYN720-1 : 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 : n021.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 12:21:21 CDT 2014 % % CPUTime: 0.33 % 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/SYN001-0.ax ... % % % % Proving ... % % % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % % START OF MODEL (DIG): % k0(e) % k0(b) % k1(d) % k1(c) % k1(a) % k1(e) % k1(b) % k2(_0, _0) % k2(_0, d) % k2(a, e) % k2(a, b) % k2(c, a) % k2(c, e) % k2(c, b) % k2(b, c) % k2(b, a) % k2(b, e) % k2(e, c) % k2(e, a) % k2(e, b) % k3(_0, _0, _0) % k3(_0, _0, d) % k3(_0, _0, c) % k3(_0, _0, b) % k3(_0, _0, e) % k3(_0, d, _0) % k3(d, d, _0) % k3(d, c, d) % k3(d, a, d) % k3(d, b, d) % k3(d, e, d) % k3(a, _0, a) % k3(a, a, _0) % k3(c, _0, c) % k3(e, _0, e) % k3(e, e, a) % k3(b, _0, b) % k3(b, b, a) % k4(c) % k4(e) % k5(_0) % l0(a) % l0(c) % l1(d, _0) % l1(c, c) % l1(a, a) % l1(e, e) % l1(b, b) % l1(b, e) % l2(_0, _0) % l2(_0, e) % l2(_0, b) % l3(_0, _0) % l3(d, c) % l3(e, d) % l3(e, a) % l3(e, c) % l3(e, b) % l3(b, a) % l3(b, c) % l3(b, e) % l4(_0) % l5(d) % l5(c) % l5(a) % l5(e) % l5(b) % m0(_0, d, _1) % m0(d, e, c) % m0(a, _0, a) % m0(a, e, e) % m0(c, b, a) % m0(e, b, c) % m0(b, a, a) % m0(b, b, e) % m1(_0, _0, _0) % m1(_0, d, _0) % m1(_0, d, d) % m1(d, a, c) % m1(d, a, a) % m1(d, a, b) % m1(d, c, c) % m1(d, e, e) % m1(d, b, b) % m1(a, a, b) % m1(a, e, a) % m1(a, b, a) % m1(a, b, b) % m1(c, a, a) % m1(c, e, c) % m1(c, b, c) % m1(b, _0, b) % m1(b, a, a) % m1(b, a, e) % m1(b, c, c) % m1(b, b, e) % m1(b, e, e) % m1(e, _0, e) % m1(e, a, a) % m1(e, b, b) % m2(d) % m2(b) % m3(_0, _0, _0) % m3(_0, d, d) % m3(_0, b, b) % m3(_0, e, e) % m3(d, d, c) % m3(d, d, a) % m3(d, _0, d) % m3(c, d, c) % m3(c, a, c) % m3(c, c, a) % m3(c, b, d) % m3(c, b, c) % m3(c, e, c) % m3(a, _0, a) % m3(a, a, c) % m3(b, _0, b) % m3(b, b, c) % m3(b, b, a) % m3(e, _0, e) % m3(e, e, c) % m3(e, e, a) % m4(_0, _1) % m5(_0, _1) % n0(d, c) % n0(d, e) % n0(d, b) % n0(a, b) % n0(c, d) % n0(e, b) % n0(e, e) % n0(b, a) % n1(_0, _0, _1) % n1(d, c, d) % n1(d, e, e) % n1(a, _0, _0) % n1(a, _0, a) % n1(c, _0, _0) % n1(c, _0, c) % n1(b, a, b) % n1(b, c, b) % n1(b, e, e) % n1(e, a, e) % n1(e, c, e) % n2(_0) % n3(_0) % n4(d, _0) % n4(_0, _0) % n4(_0, a) % n4(_0, b) % n4(_0, e) % n4(b, c) % n4(e, _0) % n5(_0, _1) % p0(c, b) % p0(b, _0) % p1(_0, _0, _0) % p1(_0, _1, a) % p1(_0, _0, b) % p1(_0, d, _0) % p1(d, _0, _1) % p1(c, c, e) % p1(c, b, c) % p1(a, _0, b) % p1(b, _0, c) % p1(b, _0, b) % p1(b, b, e) % p1(e, _0, d) % p1(e, c, e) % p1(e, b, e) % p1(e, b, b) % p2(_0, _0, _0) % p2(_0, a, _0) % p2(_0, a, a) % p2(_0, b, _0) % p2(_0, b, b) % p2(_0, e, _0) % p2(_0, e, e) % p2(d, _0, d) % p2(d, _0, _0) % p2(e, d, _0) % p2(e, c, c) % p2(e, c, e) % p2(e, e, d) % p2(e, e, c) % p2(e, e, b) % p2(b, c, c) % p2(b, c, a) % p2(b, c, b) % p3(d, _0, _0) % p3(d, _0, d) % p3(d, a, e) % p3(d, a, b) % p3(d, c, a) % p3(d, c, e) % p3(d, c, b) % p3(d, b, c) % p3(d, b, a) % p3(d, b, e) % p3(d, e, c) % p3(d, e, a) % p3(d, e, b) % p3(_0, _0, _0) % p3(_0, a, a) % p3(_0, b, b) % p3(_0, e, e) % p3(a, a, _0) % p3(c, c, _0) % p3(b, c, c) % p3(b, c, b) % p3(e, _0, _0) % p3(e, _0, d) % p3(e, a, e) % p3(e, a, b) % p3(e, c, a) % p3(e, c, e) % p3(e, c, b) % p3(e, b, c) % p3(e, b, a) % p3(e, b, e) % p3(e, e, c) % p3(e, e, a) % p3(e, e, b) % p4(_0, _0, _0) % p4(_0, d, _0) % p4(_0, c, _0) % p4(_0, b, _0) % p4(_0, e, _0) % p4(d, _0, d) % p4(d, a, a) % p4(d, c, c) % p4(d, b, b) % p4(d, e, e) % p4(c, c, a) % p4(c, b, b) % p4(c, e, e) % p4(a, _0, a) % p4(a, c, c) % p4(b, d, d) % p4(b, a, a) % p4(b, a, b) % p4(b, c, c) % p4(b, b, _0) % p4(b, e, e) % p4(e, a, a) % p4(e, a, e) % p4(e, e, _0) % p5(_0, _1, _1) % p5(_0, _1, _0) % p5(_0, _0, d) % p5(_0, _0, c) % p5(_0, _0, a) % p5(_0, _0, e) % p5(_0, _0, b) % q0(_0, d) % q0(d, c) % q0(d, b) % q0(a, b) % q0(b, b) % q0(b, e) % q1(_0, _0, _0) % q1(_0, _0, d) % q1(_0, d, _0) % q1(_0, c, _0) % q1(_0, a, _0) % q1(_0, b, _0) % q1(_0, b, b) % q1(_0, e, _0) % q1(d, d, _0) % q1(a, d, d) % q1(a, a, b) % q1(a, e, e) % q1(c, d, d) % q1(c, c, a) % q1(c, a, a) % q1(c, e, e) % q1(e, _0, _0) % q1(e, e, a) % q1(e, e, b) % q1(b, c, c) % q1(b, b, a) % q1(b, b, c) % q1(b, b, e) % q2(_0, _0, _0) % q2(_0, _0, d) % q2(_0, e, _0) % q2(_0, e, e) % q2(_0, b, _0) % q2(_0, b, b) % q2(d, c, d) % q2(d, a, d) % q2(a, c, a) % q2(e, d, e) % q2(e, c, d) % q2(e, c, c) % q2(e, c, a) % q2(e, c, e) % q2(e, c, b) % q2(e, a, e) % q2(e, e, b) % q2(b, c, d) % q2(b, c, c) % q2(b, c, a) % q2(b, c, b) % q2(b, c, e) % q2(b, a, b) % q3(d, d) % q3(d, c) % q3(d, e) % q3(d, b) % q3(c, d) % q3(c, c) % q3(a, a) % q3(a, b) % q3(b, d) % q3(b, a) % q3(b, b) % q3(b, e) % q3(e, d) % q3(e, e) % q3(e, b) % q4(_0, _0) % q4(_0, e) % q4(_0, b) % q4(d, _0) % q4(a, c) % q4(e, d) % q4(e, c) % q4(e, a) % q4(b, c) % q4(b, a) % q5(_0, _1) % r0(b) % r0(e) % r1(_0) % r2(a) % r2(c) % r3(_0, _0, _0) % r3(_0, a, _0) % r3(_0, b, _0) % r3(_0, e, _0) % r3(d, _0, d) % r3(d, d, b) % r3(d, c, c) % r3(d, b, c) % r3(d, e, c) % r3(a, c, a) % r3(a, c, c) % r3(a, a, d) % r3(a, a, e) % r3(a, a, b) % r3(a, b, c) % r3(a, e, c) % r3(c, d, d) % r3(c, c, d) % r3(c, c, a) % r3(c, c, b) % r3(c, a, a) % r3(c, b, a) % r3(c, b, b) % r3(c, e, a) % r3(c, e, e) % r3(b, d, d) % r3(b, c, c) % r3(b, c, b) % r3(b, a, a) % r3(b, b, d) % r3(b, b, c) % r3(b, e, c) % r3(b, e, e) % r3(e, _0, e) % r3(e, d, d) % r3(e, c, c) % r3(e, a, a) % r3(e, b, c) % r3(e, b, b) % r3(e, e, d) % r3(e, e, c) % r3(e, e, b) % r4(_0) % r5(_0, _1) % s0(d) % s0(b) % s1(_0) % s2(d) % s2(c) % s2(a) % s2(b) % s2(e) % s3(d, _0) % s3(c, _0) % s3(a, _0) % s3(b, _0) % s3(e, _0) % s4(d) % s4(c) % s4(a) % s4(e) % s4(b) % s5(_0) % true % END OF MODEL % EOF %------------------------------------------------------------------------------