%------------------------------------------------------------------------------ % File : CARINE---0.734 % Problem : RNG001-3 : TPTP v5.0.0. Released v1.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 04:26:30 EST 2010 % Result : Unsatisfiable 20.49s % Output : Refutation 20.49s % 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/SystemOnTPTP13617/RNG/RNG001-3+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 = 0] [nf = 0] [nu = 0] [ut = 4] % Looking for a proof at depth = 2 ... % t = 0 secs [nr = 12] [nf = 18] [nu = 0] [ut = 4] % Looking for a proof at depth = 3 ... % t = 0 secs [nr = 30001] [nf = 48] [nu = 27399] [ut = 101] % Looking for a proof at depth = 4 ... % t = 0 secs [nr = 98809] [nf = 78] [nu = 92383] [ut = 101] % Looking for a proof at depth = 5 ... % t = 0 secs [nr = 167617] [nf = 108] [nu = 157367] [ut = 101] % Looking for a proof at depth = 6 ... % t = 0 secs [nr = 236425] [nf = 138] [nu = 222351] [ut = 101] % Looking for a proof at depth = 7 ... % t = 0 secs [nr = 305233] [nf = 168] [nu = 287335] [ut = 101] % Looking for a proof at depth = 8 ... % t = 0 secs [nr = 374041] [nf = 198] [nu = 352319] [ut = 101] % Looking for a proof at depth = 9 ... % t = 1 secs [nr = 442849] [nf = 228] [nu = 417303] [ut = 101] % Looking for a proof at depth = 10 ... % t = 1 secs [nr = 511657] [nf = 258] [nu = 482287] [ut = 101] % Looking for a proof at depth = 11 ... % t = 1 secs [nr = 580465] [nf = 288] [nu = 547271] [ut = 101] % Looking for a proof at depth = 12 ... % t = 1 secs [nr = 649273] [nf = 318] [nu = 612255] [ut = 101] % Looking for a proof at depth = 13 ... % t = 1 secs [nr = 718081] [nf = 348] [nu = 677239] [ut = 101] % Looking for a proof at depth = 14 ... % t = 1 secs [nr = 786889] [nf = 378] [nu = 742223] [ut = 101] % Looking for a proof at depth = 15 ... % t = 1 secs [nr = 855697] [nf = 408] [nu = 807207] [ut = 101] % Looking for a proof at depth = 16 ... % t = 1 secs [nr = 924505] [nf = 438] [nu = 872191] [ut = 101] % Looking for a proof at depth = 17 ... % t = 1 secs [nr = 993313] [nf = 468] [nu = 937175] [ut = 101] % Looking for a proof at depth = 18 ... % t = 2 secs [nr = 1062121] [nf = 498] [nu = 1002159] [ut = 101] % Looking for a proof at depth = 19 ... % t = 2 secs [nr = 1130929] [nf = 528] [nu = 1067143] [ut = 101] % Looking for a proof at depth = 20 ... % t = 2 secs [nr = 1199737] [nf = 558] [nu = 1132127] [ut = 101] % Looking for a proof at depth = 21 ... % t = 2 secs [nr = 1268545] [nf = 588] [nu = 1197111] [ut = 101] % Looking for a proof at depth = 22 ... % t = 2 secs [nr = 1337353] [nf = 618] [nu = 1262095] [ut = 101] % Looking for a proof at depth = 23 ... % t = 2 secs [nr = 1406161] [nf = 648] [nu = 1327079] [ut = 101] % Looking for a proof at depth = 24 ... % t = 2 secs [nr = 1474969] [nf = 678] [nu = 1392063] [ut = 101] % Looking for a proof at depth = 25 ... % t = 2 secs [nr = 1543777] [nf = 708] [nu = 1457047] [ut = 101] % Looking for a proof at depth = 26 ... % t = 2 secs [nr = 1612585] [nf = 738] [nu = 1522031] [ut = 101] % Looking for a proof at depth = 27 ... % t = 3 secs [nr = 1681393] [nf = 768] [nu = 1587015] [ut = 101] % Looking for a proof at depth = 28 ... % t = 3 secs [nr = 1750201] [nf = 798] [nu = 1651999] [ut = 101] % Looking for a proof at depth = 29 ... % t = 3 secs [nr = 1819009] [nf = 828] [nu = 1716983] [ut = 101] % Looking for a proof at depth = 30 ... % t = 3 secs [nr = 1887817] [nf = 858] [nu = 1781967] [ut = 101] % Restarting search with different parameters. % Looking for a proof at depth = 1 ... % t = 3 secs [nr = 1887817] [nf = 858] [nu = 1781967] [ut = 101] % Looking for a proof at depth = 2 ... % t = 3 secs [nr = 1887829] [nf = 876] [nu = 1781967] [ut = 101] % Looking for a proof at depth = 3 ... % t = 4 secs [nr = 2041652] [nf = 928] [nu = 1929788] [ut = 159] % Looking for a proof at depth = 4 ... % t = 7 secs [nr = 2676616] [nf = 990] [nu = 2445938] [ut = 277] % Looking for a proof at depth = 5 ... % t = 12 secs [nr = 3993455] [nf = 2941] [nu = 3598512] [ut = 277] % Looking for a proof at depth = 6 ... % +================================================+ % | | % | Congratulations!!! ........ A proof was found. | % | | % +================================================+ % Base Clauses and Unit Clauses used in proof: % ============================================ % Base Clauses: % ------------- % B0: ~product_3(a_0(),additive_identity_0(),additive_identity_0()) % B1: product_3(x0,x1,multiply_2(x0,x1)) % B2: sum_3(additive_identity_0(),x0,x0) % B3: sum_3(additive_inverse_1(x0),x0,additive_identity_0()) % B4: ~sum_3(x0,x4,x5) | ~sum_3(x1,x3,x4) | ~sum_3(x0,x1,x2) | sum_3(x2,x3,x5) % B5: ~sum_3(x2,x3,x5) | ~sum_3(x1,x3,x4) | ~sum_3(x0,x1,x2) | sum_3(x0,x4,x5) % B6: ~product_3(x0,x3,x4) | ~product_3(x0,x1,x2) | ~sum_3(x2,x4,x6) | ~sum_3(x1,x3,x5) | product_3(x0,x5,x6) % B7: ~product_3(x0,x5,x6) | ~product_3(x0,x3,x4) | ~product_3(x0,x1,x2) | ~sum_3(x1,x3,x5) | sum_3(x2,x4,x6) % Unit Clauses: % -------------- % U1: < d0 v4 dv2 f1 c0 t5 td2 b > product_3(x0,x1,multiply_2(x0,x1)) % U2: < d0 v2 dv1 f0 c1 t3 td1 b > sum_3(additive_identity_0(),x0,x0) % U3: < d0 v2 dv1 f1 c1 t4 td2 b > sum_3(additive_inverse_1(x0),x0,additive_identity_0()) % U6: < d3 v2 dv1 f2 c1 t5 td3 > sum_3(additive_inverse_1(additive_inverse_1(x0)),additive_identity_0(),x0) % U10: < d3 v2 dv1 f3 c1 t6 td4 > sum_3(additive_inverse_1(additive_inverse_1(additive_inverse_1(x0))),x0,additive_identity_0()) % U21: < d3 v2 dv1 f1 c1 t4 td2 > sum_3(x0,additive_inverse_1(x0),additive_identity_0()) % U29: < d3 v2 dv1 f2 c1 t5 td3 > sum_3(additive_identity_0(),x0,additive_inverse_1(additive_inverse_1(x0))) % U31: < d3 v2 dv1 f2 c1 t5 td3 > sum_3(additive_identity_0(),additive_inverse_1(additive_inverse_1(x0)),x0) % U62: < d3 v2 dv1 f0 c1 t3 td1 > sum_3(x0,additive_identity_0(),x0) % U69: < d3 v2 dv1 f2 c1 t5 td3 > sum_3(x0,additive_identity_0(),additive_inverse_1(additive_inverse_1(x0))) % U159: < d4 v0 dv0 f2 c5 t7 td2 > ~sum_3(multiply_2(a_0(),additive_identity_0()),multiply_2(a_0(),additive_identity_0()),additive_identity_0()) % U234: < d4 v3 dv1 f3 c3 t9 td2 > sum_3(multiply_2(x0,additive_identity_0()),multiply_2(x0,additive_identity_0()),multiply_2(x0,additive_identity_0())) % U277: < d6 v3 dv1 f5 c3 t11 td4 > sum_3(additive_inverse_1(additive_inverse_1(multiply_2(x0,additive_identity_0()))),multiply_2(x0,additive_identity_0()),multiply_2(x0,additive_identity_0())) % U278: < d6 v3 dv1 f5 c3 t11 td4 > sum_3(multiply_2(x0,additive_identity_0()),additive_inverse_1(additive_inverse_1(multiply_2(x0,additive_identity_0()))),multiply_2(x0,additive_identity_0())) % U286: < d6 v0 dv0 f3 c5 t8 td3 > ~sum_3(additive_identity_0(),additive_inverse_1(multiply_2(a_0(),additive_identity_0())),multiply_2(a_0(),additive_identity_0())) % U319: < d6 v1 dv1 f3 c3 t7 td4 > sum_3(additive_identity_0(),additive_inverse_1(additive_inverse_1(multiply_2(x0,additive_identity_0()))),additive_identity_0()) % U356: < d6 v2 dv1 f3 c3 t8 td3 > sum_3(additive_identity_0(),additive_inverse_1(multiply_2(x0,additive_identity_0())),multiply_2(x0,additive_identity_0())) % --------------- Start of Proof --------------- % Derivation of unit clause U1: % product_3(x0,x1,multiply_2(x0,x1)) ....... U1 % Derivation of unit clause U2: % sum_3(additive_identity_0(),x0,x0) ....... U2 % Derivation of unit clause U3: % sum_3(additive_inverse_1(x0),x0,additive_identity_0()) ....... U3 % Derivation of unit clause U6: % sum_3(additive_identity_0(),x0,x0) ....... B2 % ~sum_3(x2,x3,x5) | ~sum_3(x1,x3,x4) | ~sum_3(x0,x1,x2) | sum_3(x0,x4,x5) ....... B5 % ~sum_3(x0, x1, x2) | ~sum_3(x3, x0, additive_identity_0()) | sum_3(x3, x2, x1) ....... R1 [B2:L0, B5:L0] % sum_3(additive_inverse_1(x0),x0,additive_identity_0()) ....... U3 % ~sum_3(x0, additive_inverse_1(x1), additive_identity_0()) | sum_3(x0, additive_identity_0(), x1) ....... R2 [R1:L0, U3:L0] % sum_3(additive_inverse_1(x0),x0,additive_identity_0()) ....... U3 % sum_3(additive_inverse_1(additive_inverse_1(x0)), additive_identity_0(), x0) ....... R3 [R2:L0, U3:L0] % Derivation of unit clause U10: % sum_3(additive_identity_0(),x0,x0) ....... B2 % ~sum_3(x2,x3,x5) | ~sum_3(x1,x3,x4) | ~sum_3(x0,x1,x2) | sum_3(x0,x4,x5) ....... B5 % ~sum_3(x0, x1, x2) | ~sum_3(x3, x0, additive_identity_0()) | sum_3(x3, x2, x1) ....... R1 [B2:L0, B5:L0] % sum_3(additive_inverse_1(additive_inverse_1(x0)),additive_identity_0(),x0) ....... U6 % ~sum_3(x0, additive_inverse_1(additive_inverse_1(x1)), additive_identity_0()) | sum_3(x0, x1, additive_identity_0()) ....... R2 [R1:L0, U6:L0] % sum_3(additive_inverse_1(x0),x0,additive_identity_0()) ....... U3 % sum_3(additive_inverse_1(additive_inverse_1(additive_inverse_1(x0))), x0, additive_identity_0()) ....... R3 [R2:L0, U3:L0] % Derivation of unit clause U21: % sum_3(additive_inverse_1(x0),x0,additive_identity_0()) ....... B3 % ~sum_3(x0,x4,x5) | ~sum_3(x1,x3,x4) | ~sum_3(x0,x1,x2) | sum_3(x2,x3,x5) ....... B4 % ~sum_3(x0, x1, x2) | ~sum_3(additive_inverse_1(x2), x0, x3) | sum_3(x3, x1, additive_identity_0()) ....... R1 [B3:L0, B4:L0] % sum_3(additive_identity_0(),x0,x0) ....... U2 % ~sum_3(additive_inverse_1(x0), additive_identity_0(), x1) | sum_3(x1, x0, additive_identity_0()) ....... R2 [R1:L0, U2:L0] % sum_3(additive_inverse_1(additive_inverse_1(x0)),additive_identity_0(),x0) ....... U6 % sum_3(x0, additive_inverse_1(x0), additive_identity_0()) ....... R3 [R2:L0, U6:L0] % Derivation of unit clause U29: % sum_3(additive_inverse_1(x0),x0,additive_identity_0()) ....... B3 % ~sum_3(x0,x4,x5) | ~sum_3(x1,x3,x4) | ~sum_3(x0,x1,x2) | sum_3(x2,x3,x5) ....... B4 % ~sum_3(x0, additive_identity_0(), x1) | ~sum_3(x0, additive_inverse_1(x2), x3) | sum_3(x3, x2, x1) ....... R1 [B3:L0, B4:L1] % sum_3(additive_inverse_1(additive_inverse_1(x0)),additive_identity_0(),x0) ....... U6 % ~sum_3(additive_inverse_1(additive_inverse_1(x0)), additive_inverse_1(x1), x2) | sum_3(x2, x1, x0) ....... R2 [R1:L0, U6:L0] % sum_3(additive_inverse_1(additive_inverse_1(additive_inverse_1(x0))),x0,additive_identity_0()) ....... U10 % sum_3(additive_identity_0(), x0, additive_inverse_1(additive_inverse_1(x0))) ....... R3 [R2:L0, U10:L0] % Derivation of unit clause U31: % sum_3(additive_inverse_1(x0),x0,additive_identity_0()) ....... B3 % ~sum_3(x0,x4,x5) | ~sum_3(x1,x3,x4) | ~sum_3(x0,x1,x2) | sum_3(x2,x3,x5) ....... B4 % ~sum_3(x0, additive_identity_0(), x1) | ~sum_3(x0, additive_inverse_1(x2), x3) | sum_3(x3, x2, x1) ....... R1 [B3:L0, B4:L1] % sum_3(additive_inverse_1(additive_inverse_1(x0)),additive_identity_0(),x0) ....... U6 % ~sum_3(additive_inverse_1(additive_inverse_1(x0)), additive_inverse_1(x1), x2) | sum_3(x2, x1, x0) ....... R2 [R1:L0, U6:L0] % sum_3(x0,additive_inverse_1(x0),additive_identity_0()) ....... U21 % sum_3(additive_identity_0(), additive_inverse_1(additive_inverse_1(x0)), x0) ....... R3 [R2:L0, U21:L0] % Derivation of unit clause U62: % sum_3(additive_inverse_1(x0),x0,additive_identity_0()) ....... B3 % ~sum_3(x2,x3,x5) | ~sum_3(x1,x3,x4) | ~sum_3(x0,x1,x2) | sum_3(x0,x4,x5) ....... B5 % ~sum_3(x0, x1, x2) | ~sum_3(x3, additive_inverse_1(x1), x0) | sum_3(x3, additive_identity_0(), x2) ....... R1 [B3:L0, B5:L1] % sum_3(additive_identity_0(),x0,x0) ....... U2 % ~sum_3(x0, additive_inverse_1(x1), additive_identity_0()) | sum_3(x0, additive_identity_0(), x1) ....... R2 [R1:L0, U2:L0] % sum_3(x0,additive_inverse_1(x0),additive_identity_0()) ....... U21 % sum_3(x0, additive_identity_0(), x0) ....... R3 [R2:L0, U21:L0] % Derivation of unit clause U69: % sum_3(additive_inverse_1(x0),x0,additive_identity_0()) ....... B3 % ~sum_3(x2,x3,x5) | ~sum_3(x1,x3,x4) | ~sum_3(x0,x1,x2) | sum_3(x0,x4,x5) ....... B5 % ~sum_3(x0, x1, x2) | ~sum_3(x3, additive_inverse_1(x1), x0) | sum_3(x3, additive_identity_0(), x2) ....... R1 [B3:L0, B5:L1] % sum_3(additive_identity_0(),x0,additive_inverse_1(additive_inverse_1(x0))) ....... U29 % ~sum_3(x0, additive_inverse_1(x1), additive_identity_0()) | sum_3(x0, additive_identity_0(), additive_inverse_1(additive_inverse_1(x1))) ....... R2 [R1:L0, U29:L0] % sum_3(x0,additive_inverse_1(x0),additive_identity_0()) ....... U21 % sum_3(x0, additive_identity_0(), additive_inverse_1(additive_inverse_1(x0))) ....... R3 [R2:L0, U21:L0] % Derivation of unit clause U159: % ~product_3(a_0(),additive_identity_0(),additive_identity_0()) ....... B0 % ~product_3(x0,x3,x4) | ~product_3(x0,x1,x2) | ~sum_3(x2,x4,x6) | ~sum_3(x1,x3,x5) | product_3(x0,x5,x6) ....... B6 % ~product_3(a_0(), x0, x1) | ~product_3(a_0(), x2, x3) | ~sum_3(x3, x1, additive_identity_0()) | ~sum_3(x2, x0, additive_identity_0()) ....... R1 [B0:L0, B6:L4] % ~product_3(a_0(), x0, x1) | ~sum_3(x1, x1, additive_identity_0()) | ~sum_3(x0, x0, additive_identity_0()) ....... R2 [R1:L1, R1:L0] % product_3(x0,x1,multiply_2(x0,x1)) ....... U1 % ~sum_3(multiply_2(a_0(), x0), multiply_2(a_0(), x0), additive_identity_0()) | ~sum_3(x0, x0, additive_identity_0()) ....... R3 [R2:L0, U1:L0] % sum_3(additive_identity_0(),x0,x0) ....... U2 % ~sum_3(multiply_2(a_0(), additive_identity_0()), multiply_2(a_0(), additive_identity_0()), additive_identity_0()) ....... R4 [R3:L1, U2:L0] % Derivation of unit clause U234: % product_3(x0,x1,multiply_2(x0,x1)) ....... B1 % ~product_3(x0,x5,x6) | ~product_3(x0,x3,x4) | ~product_3(x0,x1,x2) | ~sum_3(x1,x3,x5) | sum_3(x2,x4,x6) ....... B7 % ~product_3(x0, x1, x2) | ~product_3(x0, x3, x4) | ~sum_3(x3, x1, x5) | sum_3(x4, x2, multiply_2(x0, x5)) ....... R1 [B1:L0, B7:L0] % ~product_3(x0, x1, x2) | ~sum_3(x1, x1, x3) | sum_3(x2, x2, multiply_2(x0, x3)) ....... R2 [R1:L1, R1:L0] % product_3(x0,x1,multiply_2(x0,x1)) ....... U1 % ~sum_3(x0, x0, x1) | sum_3(multiply_2(x2, x0), multiply_2(x2, x0), multiply_2(x2, x1)) ....... R3 [R2:L0, U1:L0] % sum_3(additive_identity_0(),x0,x0) ....... U2 % sum_3(multiply_2(x0, additive_identity_0()), multiply_2(x0, additive_identity_0()), multiply_2(x0, additive_identity_0())) ....... R4 [R3:L0, U2:L0] % Derivation of unit clause U277: % sum_3(additive_identity_0(),x0,x0) ....... B2 % ~sum_3(x0,x4,x5) | ~sum_3(x1,x3,x4) | ~sum_3(x0,x1,x2) | sum_3(x2,x3,x5) ....... B4 % ~sum_3(x0, x1, x2) | ~sum_3(additive_identity_0(), x0, x3) | sum_3(x3, x1, x2) ....... R1 [B2:L0, B4:L0] % ~sum_3(x0,x4,x5) | ~sum_3(x1,x3,x4) | ~sum_3(x0,x1,x2) | sum_3(x2,x3,x5) ....... B4 % ~sum_3(x0, x1, x2) | ~sum_3(additive_identity_0(), x0, x3) | ~sum_3(x4, x5, x1) | ~sum_3(x3, x4, x6) | sum_3(x6, x5, x2) ....... R2 [R1:L2, B4:L0] % ~sum_3(x0, x1, x2) | ~sum_3(additive_identity_0(), x0, x1) | ~sum_3(x1, additive_identity_0(), x3) | sum_3(x3, x0, x2) ....... R3 [R2:L1, R2:L2] % sum_3(multiply_2(x0,additive_identity_0()),multiply_2(x0,additive_identity_0()),multiply_2(x0,additive_identity_0())) ....... U234 % ~sum_3(additive_identity_0(), multiply_2(x0, additive_identity_0()), multiply_2(x0, additive_identity_0())) | ~sum_3(multiply_2(x0, additive_identity_0()), additive_identity_0(), x1) | sum_3(x1, multiply_2(x0, additive_identity_0()), multiply_2(x0, additive_identity_0())) ....... R4 [R3:L0, U234:L0] % sum_3(additive_identity_0(),x0,x0) ....... U2 % ~sum_3(multiply_2(x0, additive_identity_0()), additive_identity_0(), x1) | sum_3(x1, multiply_2(x0, additive_identity_0()), multiply_2(x0, additive_identity_0())) ....... R5 [R4:L0, U2:L0] % sum_3(x0,additive_identity_0(),additive_inverse_1(additive_inverse_1(x0))) ....... U69 % sum_3(additive_inverse_1(additive_inverse_1(multiply_2(x0, additive_identity_0()))), multiply_2(x0, additive_identity_0()), multiply_2(x0, additive_identity_0())) ....... R6 [R5:L0, U69:L0] % Derivation of unit clause U278: % sum_3(additive_identity_0(),x0,x0) ....... B2 % ~sum_3(x0,x4,x5) | ~sum_3(x1,x3,x4) | ~sum_3(x0,x1,x2) | sum_3(x2,x3,x5) ....... B4 % ~sum_3(x0, x1, x2) | ~sum_3(additive_identity_0(), x0, x3) | sum_3(x3, x1, x2) ....... R1 [B2:L0, B4:L0] % ~sum_3(x0,x4,x5) | ~sum_3(x1,x3,x4) | ~sum_3(x0,x1,x2) | sum_3(x2,x3,x5) ....... B4 % ~sum_3(x0, x1, x2) | ~sum_3(additive_identity_0(), x0, x3) | ~sum_3(x4, x5, x1) | ~sum_3(x3, x4, x6) | sum_3(x6, x5, x2) ....... R2 [R1:L2, B4:L0] % ~sum_3(x0, x1, x2) | ~sum_3(additive_identity_0(), x0, x1) | ~sum_3(x1, additive_identity_0(), x3) | sum_3(x3, x0, x2) ....... R3 [R2:L1, R2:L2] % sum_3(additive_inverse_1(additive_inverse_1(multiply_2(x0,additive_identity_0()))),multiply_2(x0,additive_identity_0()),multiply_2(x0,additive_identity_0())) ....... U277 % ~sum_3(additive_identity_0(), additive_inverse_1(additive_inverse_1(multiply_2(x0, additive_identity_0()))), multiply_2(x0, additive_identity_0())) | ~sum_3(multiply_2(x0, additive_identity_0()), additive_identity_0(), x1) | sum_3(x1, additive_inverse_1(additive_inverse_1(multiply_2(x0, additive_identity_0()))), multiply_2(x0, additive_identity_0())) ....... R4 [R3:L0, U277:L0] % sum_3(additive_identity_0(),additive_inverse_1(additive_inverse_1(x0)),x0) ....... U31 % ~sum_3(multiply_2(x0, additive_identity_0()), additive_identity_0(), x1) | sum_3(x1, additive_inverse_1(additive_inverse_1(multiply_2(x0, additive_identity_0()))), multiply_2(x0, additive_identity_0())) ....... R5 [R4:L0, U31:L0] % sum_3(x0,additive_identity_0(),x0) ....... U62 % sum_3(multiply_2(x0, additive_identity_0()), additive_inverse_1(additive_inverse_1(multiply_2(x0, additive_identity_0()))), multiply_2(x0, additive_identity_0())) ....... R6 [R5:L0, U62:L0] % Derivation of unit clause U286: % sum_3(additive_identity_0(),x0,x0) ....... B2 % ~sum_3(x0,x4,x5) | ~sum_3(x1,x3,x4) | ~sum_3(x0,x1,x2) | sum_3(x2,x3,x5) ....... B4 % ~sum_3(x0, x1, x2) | ~sum_3(additive_identity_0(), x0, x3) | sum_3(x3, x1, x2) ....... R1 [B2:L0, B4:L0] % ~sum_3(x0,x4,x5) | ~sum_3(x1,x3,x4) | ~sum_3(x0,x1,x2) | sum_3(x2,x3,x5) ....... B4 % ~sum_3(x0, x1, x2) | ~sum_3(additive_identity_0(), x0, x3) | ~sum_3(x4, x5, x1) | ~sum_3(x3, x4, x6) | sum_3(x6, x5, x2) ....... R2 [R1:L2, B4:L0] % ~sum_3(x0, x1, x2) | ~sum_3(additive_identity_0(), x0, x3) | ~sum_3(x3, x3, x1) | sum_3(x1, x3, x2) ....... R3 [R2:L3, R2:L2] % sum_3(additive_inverse_1(x0),x0,additive_identity_0()) ....... U3 % ~sum_3(additive_identity_0(), additive_inverse_1(x0), x1) | ~sum_3(x1, x1, x0) | sum_3(x0, x1, additive_identity_0()) ....... R4 [R3:L0, U3:L0] % sum_3(multiply_2(x0,additive_identity_0()),multiply_2(x0,additive_identity_0()),multiply_2(x0,additive_identity_0())) ....... U234 % ~sum_3(additive_identity_0(), additive_inverse_1(multiply_2(x0, additive_identity_0())), multiply_2(x0, additive_identity_0())) | sum_3(multiply_2(x0, additive_identity_0()), multiply_2(x0, additive_identity_0()), additive_identity_0()) ....... R5 [R4:L1, U234:L0] % ~sum_3(multiply_2(a_0(),additive_identity_0()),multiply_2(a_0(),additive_identity_0()),additive_identity_0()) ....... U159 % ~sum_3(additive_identity_0(), additive_inverse_1(multiply_2(a_0(), additive_identity_0())), multiply_2(a_0(), additive_identity_0())) ....... R6 [R5:L1, U159:L0] % Derivation of unit clause U319: % sum_3(additive_identity_0(),x0,x0) ....... B2 % ~sum_3(x0,x4,x5) | ~sum_3(x1,x3,x4) | ~sum_3(x0,x1,x2) | sum_3(x2,x3,x5) ....... B4 % ~sum_3(x0, x1, x2) | ~sum_3(additive_identity_0(), x0, x3) | sum_3(x3, x1, x2) ....... R1 [B2:L0, B4:L0] % ~sum_3(x0,x4,x5) | ~sum_3(x1,x3,x4) | ~sum_3(x0,x1,x2) | sum_3(x2,x3,x5) ....... B4 % ~sum_3(x0, x1, x2) | ~sum_3(additive_identity_0(), x0, x3) | ~sum_3(x4, x5, x1) | ~sum_3(x3, x4, x6) | sum_3(x6, x5, x2) ....... R2 [R1:L2, B4:L0] % ~sum_3(additive_identity_0(), x0, x0) | ~sum_3(x1, x2, x1) | ~sum_3(x0, x1, x3) | sum_3(x3, x2, x3) ....... R3 [R2:L0, R2:L3] % sum_3(additive_identity_0(),x0,x0) ....... U2 % ~sum_3(x0, x1, x0) | ~sum_3(x2, x0, x3) | sum_3(x3, x1, x3) ....... R4 [R3:L0, U2:L0] % sum_3(multiply_2(x0,additive_identity_0()),additive_inverse_1(additive_inverse_1(multiply_2(x0,additive_identity_0()))),multiply_2(x0,additive_identity_0())) ....... U278 % ~sum_3(x0, multiply_2(x1, additive_identity_0()), x2) | sum_3(x2, additive_inverse_1(additive_inverse_1(multiply_2(x1, additive_identity_0()))), x2) ....... R5 [R4:L0, U278:L0] % sum_3(additive_inverse_1(x0),x0,additive_identity_0()) ....... U3 % sum_3(additive_identity_0(), additive_inverse_1(additive_inverse_1(multiply_2(x0, additive_identity_0()))), additive_identity_0()) ....... R6 [R5:L0, U3:L0] % Derivation of unit clause U356: % sum_3(additive_identity_0(),x0,x0) ....... B2 % ~sum_3(x0,x4,x5) | ~sum_3(x1,x3,x4) | ~sum_3(x0,x1,x2) | sum_3(x2,x3,x5) ....... B4 % ~sum_3(x0, x1, x2) | ~sum_3(additive_identity_0(), x0, x3) | sum_3(x3, x1, x2) ....... R1 [B2:L0, B4:L0] % ~sum_3(x0,x4,x5) | ~sum_3(x1,x3,x4) | ~sum_3(x0,x1,x2) | sum_3(x2,x3,x5) ....... B4 % ~sum_3(x0, x1, x2) | ~sum_3(additive_identity_0(), x0, x3) | ~sum_3(x4, x5, x1) | ~sum_3(x3, x4, x6) | sum_3(x6, x5, x2) ....... R2 [R1:L2, B4:L0] % ~sum_3(x0, x1, x2) | ~sum_3(x0, x3, x1) | ~sum_3(additive_identity_0(), x0, additive_identity_0()) | sum_3(additive_identity_0(), x3, x2) ....... R3 [R2:L1, R2:L3] % sum_3(additive_inverse_1(additive_inverse_1(x0)),additive_identity_0(),x0) ....... U6 % ~sum_3(additive_inverse_1(additive_inverse_1(x0)), x1, additive_identity_0()) | ~sum_3(additive_identity_0(), additive_inverse_1(additive_inverse_1(x0)), additive_identity_0()) | sum_3(additive_identity_0(), x1, x0) ....... R4 [R3:L0, U6:L0] % sum_3(additive_inverse_1(x0),x0,additive_identity_0()) ....... U3 % ~sum_3(additive_identity_0(), additive_inverse_1(additive_inverse_1(x0)), additive_identity_0()) | sum_3(additive_identity_0(), additive_inverse_1(x0), x0) ....... R5 [R4:L0, U3:L0] % sum_3(additive_identity_0(),additive_inverse_1(additive_inverse_1(multiply_2(x0,additive_identity_0()))),additive_identity_0()) ....... U319 % sum_3(additive_identity_0(), additive_inverse_1(multiply_2(x0, additive_identity_0())), multiply_2(x0, additive_identity_0())) ....... R6 [R5:L0, U319:L0] % Derivation of the empty clause: % sum_3(additive_identity_0(),additive_inverse_1(multiply_2(x0,additive_identity_0())),multiply_2(x0,additive_identity_0())) ....... U356 % ~sum_3(additive_identity_0(),additive_inverse_1(multiply_2(a_0(),additive_identity_0())),multiply_2(a_0(),additive_identity_0())) ....... U286 % [] ....... R1 [U356:L0, U286:L0] % --------------- End of Proof --------------- % PROOF FOUND! % --------------------------------------------- % | Statistics | % --------------------------------------------- % Profile 3: Performance Statistics: % ================================== % Total number of generated clauses: 5429548 % resolvents: 5405006 factors: 24542 % Number of unit clauses generated: 4849327 % % unit clauses generated to total clauses generated: 89.31 % Number of unit clauses constructed and retained at depth [x]: % ============================================================= % [0] = 4 [3] = 155 % [4] = 118 [6] = 80 % Total = 357 % Number of generated clauses having [x] literals: % ------------------------------------------------ % [1] = 4849327 [2] = 517865 [3] = 31109 [4] = 24582 [5] = 6611 [6] = 54 % Average size of a generated clause: 2.0 % Number of unit clauses per predicate list: % ========================================== % [0] product_3 (+)18 (-)28 % [1] sum_3 (+)245 (-)66 % ------------------ % Total: (+)263 (-)94 % Total number of unit clauses retained: 357 % Number of clauses skipped because of their length: 41791 % N base clauses skippped in resolve-with-all-base-clauses % because of the shortest resolvents table: 0 % Number of successful unifications: 5429607 % Number of unification failures: 57379650 % Number of unit to unit unification failures: 16663 % N literal unification failure due to lookup root_id table: 28856 % N base clause resolution failure due to lookup table: 140 % N UC-BCL resolution dropped due to lookup table: 0 % Max entries in substitution set: 19 % N unit clauses dropped because they exceeded max values: 1065034 % N unit clauses dropped because too much nesting: 248957 % 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: 11 % Max term depth in a unit clause: 4 % Number of states in UCFA table: 826 % Total number of terms of all unit clauses in table: 2988 % Max allowed number of states in UCFA: 80000 % Ratio n states used/total allowed states: 0.01 % Ratio n states used/total unit clauses terms: 0.28 % Number of symbols (columns) in UCFA: 40 % Profile 2: Number of calls to: % ============================== % PTUnify() = 62809257 % ConstructUnitClause() = 1065387 % Profile 1: Time spent in: % ========================= % ConstructUnitClause() : 1.37 secs % -------------------------------------------------------- % | | % Inferences per sec: 271477 % | | % -------------------------------------------------------- % Elapsed time: 20 secs % CPU time: 20.48 secs % %------------------------------------------------------------------------------