%------------------------------------------------------------------------------ % File : CARINE---0.734 % Problem : SYN312-1 : TPTP v5.0.0. Bugfixed v2.0.0. % Transfm : add_equality % Format : carine % Command : carine %s t=%d xo=off uct=32000 % Computer : art11.cs.miami.edu % Model : i686 i686 % CPU : Intel(R) Pentium(R) 4 CPU 3.00GHz @ 3000MHz % Memory : 2006MB % OS : Linux 2.6.31.5-127.fc12.i686.PAE % CPULimit : 300s % DateTime : Sun Nov 28 08:52:49 EST 2010 % Result : Unsatisfiable 0.60s % Output : Refutation 0.60s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % Command entered: % /home/graph/tptp/Systems/CARINE---0.734/carine /tmp/SystemOnTPTP17968/SYN/SYN312-1+noeq.car t=300 xo=off uct=32000 % CARINE version 0.734 (Dec 2003) % Initializing tables ... done. % Parsing ........ done. % Calculating time slices ... done. % Building Lookup Tables ... done. % Looking for a proof at depth = 1 ... % t = 0 secs [nr = 653] [nf = 0] [nu = 629] [ut = 465] % Looking for a proof at depth = 2 ... % +================================================+ % | | % | Congratulations!!! ........ A proof was found. | % | | % +================================================+ % Base Clauses and Unit Clauses used in proof: % ============================================ % Base Clauses: % ------------- % B0: p_3(f_1(b_0()),d_0(),c_0()) % B1: p_3(a_0(),f_1(b_0()),c_0()) % B2: ~p_3(x1,x0,x2) | p_3(x0,x1,x2) % B3: ~p_3(x2,x1,x0) | p_3(x0,x1,x2) % B4: ~p_3(x0,x1,x2) | p_3(x0,x1,f_1(x2)) % B5: ~p_3(x0,x1,x2) | p_3(g_1(x0),x1,x2) % B6: ~p_3(x3,x1,x2) | ~p_3(x0,x3,x2) | p_3(x0,x1,x2) % Unit Clauses: % -------------- % U2: < d0 v0 dv0 f6 c3 t9 td3 b nc > ~p_3(f_1(g_1(a_0())),f_1(g_1(d_0())),f_1(g_1(c_0()))) % U10: < d1 v0 dv0 f2 c3 t5 td2 > p_3(g_1(a_0()),f_1(b_0()),c_0()) % U114: < d1 v0 dv0 f5 c3 t8 td3 > ~p_3(f_1(g_1(a_0())),f_1(g_1(d_0())),g_1(c_0())) % U467: < d2 v0 dv0 f1 c3 t4 td2 > p_3(g_1(a_0()),d_0(),c_0()) % U917: < d2 v0 dv0 f1 c3 t4 td2 > p_3(c_0(),g_1(a_0()),d_0()) % U1361: < d2 v0 dv0 f1 c3 t4 td2 > p_3(d_0(),c_0(),g_1(a_0())) % U1378: < d2 v0 dv0 f5 c3 t8 td3 > ~p_3(f_1(g_1(d_0())),g_1(c_0()),f_1(g_1(a_0()))) % U1382: < d2 v0 dv0 f5 c3 t8 td3 > ~p_3(g_1(c_0()),f_1(g_1(a_0())),f_1(g_1(d_0()))) % U2376: < d2 v0 dv0 f2 c3 t5 td3 > p_3(c_0(),d_0(),f_1(g_1(a_0()))) % U5127: < d2 v0 dv0 f3 c3 t6 td3 > p_3(g_1(d_0()),c_0(),f_1(g_1(a_0()))) % U11732: < d2 v0 dv0 f4 c3 t7 td3 > ~p_3(f_1(g_1(a_0())),c_0(),f_1(g_1(d_0()))) % U17870: < d2 v0 dv0 f4 c3 t7 td3 > p_3(f_1(g_1(a_0())),c_0(),f_1(g_1(d_0()))) % --------------- Start of Proof --------------- % Derivation of unit clause U2: % ~p_3(f_1(g_1(a_0())),f_1(g_1(d_0())),f_1(g_1(c_0()))) ....... U2 % Derivation of unit clause U10: % p_3(a_0(),f_1(b_0()),c_0()) ....... B1 % ~p_3(x0,x1,x2) | p_3(g_1(x0),x1,x2) ....... B5 % p_3(g_1(a_0()), f_1(b_0()), c_0()) ....... R1 [B1:L0, B5:L0] % Derivation of unit clause U114: % ~p_3(x0,x1,x2) | p_3(x0,x1,f_1(x2)) ....... B4 % ~p_3(f_1(g_1(a_0())),f_1(g_1(d_0())),f_1(g_1(c_0()))) ....... U2 % ~p_3(f_1(g_1(a_0())), f_1(g_1(d_0())), g_1(c_0())) ....... R1 [B4:L1, U2:L0] % Derivation of unit clause U467: % p_3(f_1(b_0()),d_0(),c_0()) ....... B0 % ~p_3(x3,x1,x2) | ~p_3(x0,x3,x2) | p_3(x0,x1,x2) ....... B6 % ~p_3(x0, f_1(b_0()), c_0()) | p_3(x0, d_0(), c_0()) ....... R1 [B0:L0, B6:L0] % p_3(g_1(a_0()),f_1(b_0()),c_0()) ....... U10 % p_3(g_1(a_0()), d_0(), c_0()) ....... R2 [R1:L0, U10:L0] % Derivation of unit clause U917: % ~p_3(x1,x0,x2) | p_3(x0,x1,x2) ....... B2 % ~p_3(x2,x1,x0) | p_3(x0,x1,x2) ....... B3 % ~p_3(x0, x1, x2) | p_3(x2, x0, x1) ....... R1 [B2:L1, B3:L0] % p_3(g_1(a_0()),d_0(),c_0()) ....... U467 % p_3(c_0(), g_1(a_0()), d_0()) ....... R2 [R1:L0, U467:L0] % Derivation of unit clause U1361: % ~p_3(x1,x0,x2) | p_3(x0,x1,x2) ....... B2 % ~p_3(x2,x1,x0) | p_3(x0,x1,x2) ....... B3 % ~p_3(x0, x1, x2) | p_3(x2, x0, x1) ....... R1 [B2:L1, B3:L0] % p_3(c_0(),g_1(a_0()),d_0()) ....... U917 % p_3(d_0(), c_0(), g_1(a_0())) ....... R2 [R1:L0, U917:L0] % Derivation of unit clause U1378: % ~p_3(x1,x0,x2) | p_3(x0,x1,x2) ....... B2 % ~p_3(x2,x1,x0) | p_3(x0,x1,x2) ....... B3 % ~p_3(x0, x1, x2) | p_3(x2, x0, x1) ....... R1 [B2:L1, B3:L0] % ~p_3(f_1(g_1(a_0())),f_1(g_1(d_0())),g_1(c_0())) ....... U114 % ~p_3(f_1(g_1(d_0())), g_1(c_0()), f_1(g_1(a_0()))) ....... R2 [R1:L1, U114:L0] % Derivation of unit clause U1382: % ~p_3(x1,x0,x2) | p_3(x0,x1,x2) ....... B2 % ~p_3(x2,x1,x0) | p_3(x0,x1,x2) ....... B3 % ~p_3(x0, x1, x2) | p_3(x2, x0, x1) ....... R1 [B2:L1, B3:L0] % ~p_3(f_1(g_1(d_0())),g_1(c_0()),f_1(g_1(a_0()))) ....... U1378 % ~p_3(g_1(c_0()), f_1(g_1(a_0())), f_1(g_1(d_0()))) ....... R2 [R1:L1, U1378:L0] % Derivation of unit clause U2376: % ~p_3(x1,x0,x2) | p_3(x0,x1,x2) ....... B2 % ~p_3(x0,x1,x2) | p_3(x0,x1,f_1(x2)) ....... B4 % ~p_3(x0, x1, x2) | p_3(x1, x0, f_1(x2)) ....... R1 [B2:L1, B4:L0] % p_3(d_0(),c_0(),g_1(a_0())) ....... U1361 % p_3(c_0(), d_0(), f_1(g_1(a_0()))) ....... R2 [R1:L0, U1361:L0] % Derivation of unit clause U5127: % ~p_3(x1,x0,x2) | p_3(x0,x1,x2) ....... B2 % ~p_3(x0,x1,x2) | p_3(g_1(x0),x1,x2) ....... B5 % ~p_3(x0, x1, x2) | p_3(g_1(x1), x0, x2) ....... R1 [B2:L1, B5:L0] % p_3(c_0(),d_0(),f_1(g_1(a_0()))) ....... U2376 % p_3(g_1(d_0()), c_0(), f_1(g_1(a_0()))) ....... R2 [R1:L0, U2376:L0] % Derivation of unit clause U11732: % ~p_3(x1,x0,x2) | p_3(x0,x1,x2) ....... B2 % ~p_3(x0,x1,x2) | p_3(g_1(x0),x1,x2) ....... B5 % ~p_3(x0, x1, x2) | p_3(g_1(x1), x0, x2) ....... R1 [B2:L1, B5:L0] % ~p_3(g_1(c_0()),f_1(g_1(a_0())),f_1(g_1(d_0()))) ....... U1382 % ~p_3(f_1(g_1(a_0())), c_0(), f_1(g_1(d_0()))) ....... R2 [R1:L1, U1382:L0] % Derivation of unit clause U17870: % ~p_3(x2,x1,x0) | p_3(x0,x1,x2) ....... B3 % ~p_3(x0,x1,x2) | p_3(x0,x1,f_1(x2)) ....... B4 % ~p_3(x0, x1, x2) | p_3(x2, x1, f_1(x0)) ....... R1 [B3:L1, B4:L0] % p_3(g_1(d_0()),c_0(),f_1(g_1(a_0()))) ....... U5127 % p_3(f_1(g_1(a_0())), c_0(), f_1(g_1(d_0()))) ....... R2 [R1:L0, U5127:L0] % Derivation of the empty clause: % p_3(f_1(g_1(a_0())),c_0(),f_1(g_1(d_0()))) ....... U17870 % ~p_3(f_1(g_1(a_0())),c_0(),f_1(g_1(d_0()))) ....... U11732 % [] ....... R1 [U17870:L0, U11732:L0] % --------------- End of Proof --------------- % PROOF FOUND! % --------------------------------------------- % | Statistics | % --------------------------------------------- % Profile 3: Performance Statistics: % ================================== % Total number of generated clauses: 92052 % resolvents: 92048 factors: 4 % Number of unit clauses generated: 91900 % % unit clauses generated to total clauses generated: 99.83 % Number of unit clauses constructed and retained at depth [x]: % ============================================================= % [0] = 3 [1] = 462 [2] = 17406 % Total = 17871 % Number of generated clauses having [x] literals: % ------------------------------------------------ % [1] = 91900 [2] = 149 [3] = 3 % Average size of a generated clause: 2.0 % Number of unit clauses per predicate list: % ========================================== % [0] p_3 (+)17827 (-)44 % ------------------ % Total: (+)17827 (-)44 % Total number of unit clauses retained: 17871 % Number of clauses skipped because of their length: 21 % N base clauses skippped in resolve-with-all-base-clauses % because of the shortest resolvents table: 0 % Number of successful unifications: 92072 % Number of unification failures: 2001 % Number of unit to unit unification failures: 784372 % N literal unification failure due to lookup root_id table: 168 % N base clause resolution failure due to lookup table: 0 % N UC-BCL resolution dropped due to lookup table: 0 % Max entries in substitution set: 6 % N unit clauses dropped because they exceeded max values: 57824 % N unit clauses dropped because too much nesting: 10156 % N unit clauses not constrcuted because table was full: 0 % N unit clauses dropped because UCFA table was full: 0 % Max number of terms in a unit clause: 15 % Max term depth in a unit clause: 5 % Number of states in UCFA table: 19417 % Total number of terms of all unit clauses in table: 188263 % Max allowed number of states in UCFA: 136000 % Ratio n states used/total allowed states: 0.14 % Ratio n states used/total unit clauses terms: 0.10 % Number of symbols (columns) in UCFA: 41 % Profile 2: Number of calls to: % ============================== % PTUnify() = 94073 % ConstructUnitClause() = 75692 % Profile 1: Time spent in: % ========================= % ConstructUnitClause() : 0.12 secs % -------------------------------------------------------- % | | % Inferences per sec: inf % | | % -------------------------------------------------------- % Elapsed time: 1 secs % CPU time: 0.59 secs % %------------------------------------------------------------------------------