%------------------------------------------------------------------------------ % File : CARINE---0.734 % Problem : PLA031-1.001 : TPTP v5.0.0. Released v3.5.0. % Transfm : add_equality % Format : carine % Command : carine %s t=%d xo=off uct=32000 % Computer : art01.cs.miami.edu % Model : i686 i686 % CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz % Memory : 2018MB % OS : Linux 2.6.26.8-57.fc8 % CPULimit : 300s % DateTime : Sun Nov 28 03:48:14 EST 2010 % Result : Unsatisfiable 1.08s % Output : Refutation 1.08s % 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/SystemOnTPTP5655/PLA/PLA031-1.001+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 = 258] [nf = 0] [nu = 25] [ut = 94] % Looking for a proof at depth = 2 ... % t = 0 secs [nr = 9798] [nf = 0] [nu = 2732] [ut = 437] % Looking for a proof at depth = 3 ... % +================================================+ % | | % | Congratulations!!! ........ A proof was found. | % | | % +================================================+ % Base Clauses and Unit Clauses used in proof: % ============================================ % Base Clauses: % ------------- % B0: ~s_6(s2_0(),s1_0(),s2_0(),s2_0(),s2_0(),s0_0()) % B2: neq_2(truck1_0(),truck2_0()) % B25: neq_2(s1_0(),truck1_0()) % B49: neq_2(p2_0_0(),truck1_0()) % B66: path_2(s0_0(),p2_0_0()) % B68: path_2(s1_0(),p2_1_0()) % B74: path_2(p2_0_0(),s2_0()) % B76: path_2(p2_1_0(),s2_0()) % B78: link_2(s2_0(),s1_0()) % B79: link_2(s1_0(),s2_0()) % B80: link_2(s2_0(),s0_0()) % B81: link_2(s0_0(),s2_0()) % B90: ~s_6(x0,x1,truck1_0(),x3,x2,x4) | s_6(x0,x1,x2,x3,x2,x4) % B94: ~s_6(truck1_0(),x1,x2,x3,x0,x4) | s_6(x0,x1,x2,x3,x0,x4) % B97: ~path_2(x3,x6) | ~s_6(x0,x1,x2,x3,x4,x5) | s_6(x0,x1,x2,x6,x4,x5) % B99: ~link_2(x3,x5) | ~s_6(x0,x1,truck1_0(),x2,x3,x4) | s_6(x0,x1,truck1_0(),x2,x5,x4) % B100: ~link_2(x4,x5) | ~s_6(x0,x1,x2,truck2_0(),x3,x4) | s_6(x0,x1,x2,truck2_0(),x3,x5) % B103: ~neq_2(x2,truck2_0()) | ~s_6(x0,x1,x2,x3,x4,x3) | s_6(x0,x1,x2,truck2_0(),x4,x3) % B104: ~neq_2(x3,truck1_0()) | ~s_6(x0,x1,x2,x3,x2,x4) | s_6(x0,x1,truck1_0(),x3,x2,x4) % Unit Clauses: % -------------- % U77: < d0 v0 dv0 f0 c6 t6 td1 b > s_6(s2_0(),s2_0(),s0_0(),s1_0(),s0_0(),s2_0()) % U86: < d1 v0 dv0 f0 c6 t6 td1 > ~s_6(truck1_0(),s1_0(),s2_0(),s2_0(),s2_0(),s0_0()) % U92: < d1 v0 dv0 f0 c6 t6 td1 > ~s_6(truck1_0(),s1_0(),truck1_0(),s2_0(),s2_0(),s0_0()) % U98: < d2 v0 dv0 f0 c6 t6 td1 > s_6(s2_0(),s2_0(),truck1_0(),s1_0(),s0_0(),s2_0()) % U133: < d2 v0 dv0 f0 c6 t6 td1 > s_6(s2_0(),s2_0(),truck1_0(),p2_1_0(),s0_0(),s2_0()) % U206: < d2 v0 dv0 f0 c6 t6 td1 > ~s_6(truck1_0(),s1_0(),truck1_0(),p2_0_0(),s2_0(),s0_0()) % U224: < d2 v0 dv0 f0 c6 t6 td1 > s_6(s2_0(),s2_0(),truck1_0(),s2_0(),s0_0(),s2_0()) % U263: < d2 v0 dv0 f0 c6 t6 td1 > ~s_6(truck1_0(),s1_0(),truck1_0(),p2_0_0(),s1_0(),s0_0()) % U290: < d2 v0 dv0 f0 c6 t6 td1 > s_6(s2_0(),s2_0(),truck1_0(),s2_0(),s2_0(),s2_0()) % U440: < d3 v0 dv0 f0 c6 t6 td1 > s_6(s2_0(),truck1_0(),truck1_0(),truck2_0(),s2_0(),s2_0()) % U592: < d3 v0 dv0 f0 c6 t6 td1 > ~s_6(truck1_0(),truck1_0(),s1_0(),p2_0_0(),s1_0(),s0_0()) % U748: < d3 v0 dv0 f0 c6 t6 td1 > ~s_6(truck1_0(),truck1_0(),truck1_0(),s0_0(),s1_0(),s0_0()) % U1671: < d3 v0 dv0 f0 c6 t6 td1 > ~s_6(truck1_0(),truck1_0(),truck1_0(),truck2_0(),s2_0(),s0_0()) % U3213: < d3 v0 dv0 f0 c6 t6 td1 > s_6(truck1_0(),truck1_0(),truck1_0(),truck2_0(),s2_0(),s0_0()) % --------------- Start of Proof --------------- % Derivation of unit clause U77: % s_6(s2_0(),s2_0(),s0_0(),s1_0(),s0_0(),s2_0()) ....... U77 % Derivation of unit clause U86: % ~s_6(s2_0(),s1_0(),s2_0(),s2_0(),s2_0(),s0_0()) ....... B0 % ~s_6(truck1_0(),x1,x2,x3,x0,x4) | s_6(x0,x1,x2,x3,x0,x4) ....... B94 % ~s_6(truck1_0(), s1_0(), s2_0(), s2_0(), s2_0(), s0_0()) ....... R1 [B0:L0, B94:L1] % Derivation of unit clause U92: % ~s_6(x0,x1,truck1_0(),x3,x2,x4) | s_6(x0,x1,x2,x3,x2,x4) ....... B90 % ~s_6(truck1_0(),s1_0(),s2_0(),s2_0(),s2_0(),s0_0()) ....... U86 % ~s_6(truck1_0(), s1_0(), truck1_0(), s2_0(), s2_0(), s0_0()) ....... R1 [B90:L1, U86:L0] % Derivation of unit clause U98: % neq_2(s1_0(),truck1_0()) ....... B25 % ~neq_2(x3,truck1_0()) | ~s_6(x0,x1,x2,x3,x2,x4) | s_6(x0,x1,truck1_0(),x3,x2,x4) ....... B104 % ~s_6(x0, x1, x2, s1_0(), x2, x3) | s_6(x0, x1, truck1_0(), s1_0(), x2, x3) ....... R1 [B25:L0, B104:L0] % s_6(s2_0(),s2_0(),s0_0(),s1_0(),s0_0(),s2_0()) ....... U77 % s_6(s2_0(), s2_0(), truck1_0(), s1_0(), s0_0(), s2_0()) ....... R2 [R1:L0, U77:L0] % Derivation of unit clause U133: % path_2(s1_0(),p2_1_0()) ....... B68 % ~path_2(x3,x6) | ~s_6(x0,x1,x2,x3,x4,x5) | s_6(x0,x1,x2,x6,x4,x5) ....... B97 % ~s_6(x0, x1, x2, s1_0(), x3, x4) | s_6(x0, x1, x2, p2_1_0(), x3, x4) ....... R1 [B68:L0, B97:L0] % s_6(s2_0(),s2_0(),truck1_0(),s1_0(),s0_0(),s2_0()) ....... U98 % s_6(s2_0(), s2_0(), truck1_0(), p2_1_0(), s0_0(), s2_0()) ....... R2 [R1:L0, U98:L0] % Derivation of unit clause U206: % path_2(p2_0_0(),s2_0()) ....... B74 % ~path_2(x3,x6) | ~s_6(x0,x1,x2,x3,x4,x5) | s_6(x0,x1,x2,x6,x4,x5) ....... B97 % ~s_6(x0, x1, x2, p2_0_0(), x3, x4) | s_6(x0, x1, x2, s2_0(), x3, x4) ....... R1 [B74:L0, B97:L0] % ~s_6(truck1_0(),s1_0(),truck1_0(),s2_0(),s2_0(),s0_0()) ....... U92 % ~s_6(truck1_0(), s1_0(), truck1_0(), p2_0_0(), s2_0(), s0_0()) ....... R2 [R1:L1, U92:L0] % Derivation of unit clause U224: % path_2(p2_1_0(),s2_0()) ....... B76 % ~path_2(x3,x6) | ~s_6(x0,x1,x2,x3,x4,x5) | s_6(x0,x1,x2,x6,x4,x5) ....... B97 % ~s_6(x0, x1, x2, p2_1_0(), x3, x4) | s_6(x0, x1, x2, s2_0(), x3, x4) ....... R1 [B76:L0, B97:L0] % s_6(s2_0(),s2_0(),truck1_0(),p2_1_0(),s0_0(),s2_0()) ....... U133 % s_6(s2_0(), s2_0(), truck1_0(), s2_0(), s0_0(), s2_0()) ....... R2 [R1:L0, U133:L0] % Derivation of unit clause U263: % link_2(s1_0(),s2_0()) ....... B79 % ~link_2(x3,x5) | ~s_6(x0,x1,truck1_0(),x2,x3,x4) | s_6(x0,x1,truck1_0(),x2,x5,x4) ....... B99 % ~s_6(x0, x1, truck1_0(), x2, s1_0(), x3) | s_6(x0, x1, truck1_0(), x2, s2_0(), x3) ....... R1 [B79:L0, B99:L0] % ~s_6(truck1_0(),s1_0(),truck1_0(),p2_0_0(),s2_0(),s0_0()) ....... U206 % ~s_6(truck1_0(), s1_0(), truck1_0(), p2_0_0(), s1_0(), s0_0()) ....... R2 [R1:L1, U206:L0] % Derivation of unit clause U290: % link_2(s0_0(),s2_0()) ....... B81 % ~link_2(x3,x5) | ~s_6(x0,x1,truck1_0(),x2,x3,x4) | s_6(x0,x1,truck1_0(),x2,x5,x4) ....... B99 % ~s_6(x0, x1, truck1_0(), x2, s0_0(), x3) | s_6(x0, x1, truck1_0(), x2, s2_0(), x3) ....... R1 [B81:L0, B99:L0] % s_6(s2_0(),s2_0(),truck1_0(),s2_0(),s0_0(),s2_0()) ....... U224 % s_6(s2_0(), s2_0(), truck1_0(), s2_0(), s2_0(), s2_0()) ....... R2 [R1:L0, U224:L0] % Derivation of unit clause U440: % neq_2(truck1_0(),truck2_0()) ....... B2 % ~neq_2(x2,truck2_0()) | ~s_6(x0,x1,x2,x3,x4,x3) | s_6(x0,x1,x2,truck2_0(),x4,x3) ....... B103 % ~s_6(x0, x1, truck1_0(), x2, x3, x2) | s_6(x0, x1, truck1_0(), truck2_0(), x3, x2) ....... R1 [B2:L0, B103:L0] % ~s_6(x0,x1,x2,x3,x1,x4) | s_6(x0,truck1_0(),x2,x3,x1,x4) ....... B85 % ~s_6(x0, x1, truck1_0(), x2, x1, x2) | s_6(x0, truck1_0(), truck1_0(), truck2_0(), x1, x2) ....... R2 [R1:L1, B85:L0] % s_6(s2_0(),s2_0(),truck1_0(),s2_0(),s2_0(),s2_0()) ....... U290 % s_6(s2_0(), truck1_0(), truck1_0(), truck2_0(), s2_0(), s2_0()) ....... R3 [R2:L0, U290:L0] % Derivation of unit clause U592: % neq_2(p2_0_0(),truck1_0()) ....... B49 % ~neq_2(x3,truck1_0()) | ~s_6(x0,x1,x2,x3,x2,x4) | s_6(x0,x1,truck1_0(),x3,x2,x4) ....... B104 % ~s_6(x0, x1, x2, p2_0_0(), x2, x3) | s_6(x0, x1, truck1_0(), p2_0_0(), x2, x3) ....... R1 [B49:L0, B104:L0] % ~s_6(x0,truck1_0(),x2,x3,x1,x4) | s_6(x0,x1,x2,x3,x1,x4) ....... B92 % ~s_6(x0, truck1_0(), x1, p2_0_0(), x1, x2) | s_6(x0, x1, truck1_0(), p2_0_0(), x1, x2) ....... R2 [R1:L1, B92:L0] % ~s_6(truck1_0(),s1_0(),truck1_0(),p2_0_0(),s1_0(),s0_0()) ....... U263 % ~s_6(truck1_0(), truck1_0(), s1_0(), p2_0_0(), s1_0(), s0_0()) ....... R3 [R2:L1, U263:L0] % Derivation of unit clause U748: % path_2(s0_0(),p2_0_0()) ....... B66 % ~path_2(x3,x6) | ~s_6(x0,x1,x2,x3,x4,x5) | s_6(x0,x1,x2,x6,x4,x5) ....... B97 % ~s_6(x0, x1, x2, s0_0(), x3, x4) | s_6(x0, x1, x2, p2_0_0(), x3, x4) ....... R1 [B66:L0, B97:L0] % ~s_6(x0,x1,truck1_0(),x3,x2,x4) | s_6(x0,x1,x2,x3,x2,x4) ....... B90 % ~s_6(x0, x1, truck1_0(), s0_0(), x2, x3) | s_6(x0, x1, x2, p2_0_0(), x2, x3) ....... R2 [R1:L1, B90:L0] % ~s_6(truck1_0(),truck1_0(),s1_0(),p2_0_0(),s1_0(),s0_0()) ....... U592 % ~s_6(truck1_0(), truck1_0(), truck1_0(), s0_0(), s1_0(), s0_0()) ....... R3 [R2:L1, U592:L0] % Derivation of unit clause U1671: % link_2(s2_0(),s1_0()) ....... B78 % ~link_2(x3,x5) | ~s_6(x0,x1,truck1_0(),x2,x3,x4) | s_6(x0,x1,truck1_0(),x2,x5,x4) ....... B99 % ~s_6(x0, x1, truck1_0(), x2, s2_0(), x3) | s_6(x0, x1, truck1_0(), x2, s1_0(), x3) ....... R1 [B78:L0, B99:L0] % ~s_6(x0,x1,x2,truck2_0(),x4,x3) | s_6(x0,x1,x2,x3,x4,x3) ....... B89 % ~s_6(x0, x1, truck1_0(), truck2_0(), s2_0(), x2) | s_6(x0, x1, truck1_0(), x2, s1_0(), x2) ....... R2 [R1:L1, B89:L0] % ~s_6(truck1_0(),truck1_0(),truck1_0(),s0_0(),s1_0(),s0_0()) ....... U748 % ~s_6(truck1_0(), truck1_0(), truck1_0(), truck2_0(), s2_0(), s0_0()) ....... R3 [R2:L1, U748:L0] % Derivation of unit clause U3213: % link_2(s2_0(),s0_0()) ....... B80 % ~link_2(x4,x5) | ~s_6(x0,x1,x2,truck2_0(),x3,x4) | s_6(x0,x1,x2,truck2_0(),x3,x5) ....... B100 % ~s_6(x0, x1, x2, truck2_0(), x3, s2_0()) | s_6(x0, x1, x2, truck2_0(), x3, s0_0()) ....... R1 [B80:L0, B100:L0] % ~s_6(x0,x1,x2,x3,x0,x4) | s_6(truck1_0(),x1,x2,x3,x0,x4) ....... B84 % ~s_6(x0, x1, x2, truck2_0(), x0, s2_0()) | s_6(truck1_0(), x1, x2, truck2_0(), x0, s0_0()) ....... R2 [R1:L1, B84:L0] % s_6(s2_0(),truck1_0(),truck1_0(),truck2_0(),s2_0(),s2_0()) ....... U440 % s_6(truck1_0(), truck1_0(), truck1_0(), truck2_0(), s2_0(), s0_0()) ....... R3 [R2:L0, U440:L0] % Derivation of the empty clause: % s_6(truck1_0(),truck1_0(),truck1_0(),truck2_0(),s2_0(),s0_0()) ....... U3213 % ~s_6(truck1_0(),truck1_0(),truck1_0(),truck2_0(),s2_0(),s0_0()) ....... U1671 % [] ....... R1 [U3213:L0, U1671:L0] % --------------- End of Proof --------------- % PROOF FOUND! % --------------------------------------------- % | Statistics | % --------------------------------------------- % Profile 3: Performance Statistics: % ================================== % Total number of generated clauses: 67087 % resolvents: 67081 factors: 6 % Number of unit clauses generated: 30177 % % unit clauses generated to total clauses generated: 44.98 % Number of unit clauses constructed and retained at depth [x]: % ============================================================= % [0] = 84 [1] = 10 [2] = 343 [3] = 2777 % Total = 3214 % Number of generated clauses having [x] literals: % ------------------------------------------------ % [1] = 30177 [2] = 35778 [3] = 1132 % Average size of a generated clause: 2.0 % Number of unit clauses per predicate list: % ========================================== % [0] link_2 (+)6 (-)0 % [1] neq_2 (+)56 (-)8 % [2] path_2 (+)12 (-)0 % [3] s_6 (+)2477 (-)655 % ------------------ % Total: (+)2551 (-)663 % Total number of unit clauses retained: 3214 % Number of clauses skipped because of their length: 17172 % N base clauses skippped in resolve-with-all-base-clauses % because of the shortest resolvents table: 0 % Number of successful unifications: 67116 % Number of unification failures: 1320923 % Number of unit to unit unification failures: 1622785 % N literal unification failure due to lookup root_id table: 88061 % N base clause resolution failure due to lookup table: 5238 % N UC-BCL resolution dropped due to lookup table: 25513 % Max entries in substitution set: 17 % N unit clauses dropped because they exceeded max values: 21507 % N unit clauses dropped because too much nesting: 0 % 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: 6 % Max term depth in a unit clause: 1 % Number of states in UCFA table: 4209 % Total number of terms of all unit clauses in table: 18956 % Max allowed number of states in UCFA: 80000 % Ratio n states used/total allowed states: 0.05 % Ratio n states used/total unit clauses terms: 0.22 % Number of symbols (columns) in UCFA: 46 % Profile 2: Number of calls to: % ============================== % PTUnify() = 1388039 % ConstructUnitClause() = 24637 % Profile 1: Time spent in: % ========================= % ConstructUnitClause() : 0.04 secs % -------------------------------------------------------- % | | % Inferences per sec: 67087 % | | % -------------------------------------------------------- % Elapsed time: 1 secs % CPU time: 1.08 secs % %------------------------------------------------------------------------------