%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : LCL688+1.005 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % Computer : n009.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Sun Sep 27 07:55:15 AM UTC 2026 % Result : Theorem 131.08s 35.39s % Output : CNFRefutation 131.08s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL688+1.005 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.09/0.36 % Computer : n009.cluster.edu % 0.09/0.36 % Model : x86_64 x86_64 % 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.36 % Memory : 8046.5625MB % 0.09/0.36 % OS : Linux 6.8.0-71-generic % 0.09/0.36 % CPULimit : 300 % 0.03/0.36 % WCLimit : 300 % 0.03/0.36 % DateTime : Fri Sep 25 23:24:30 UTC 2026 % 0.03/0.37 % CPUTime : % 0.03/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 131.08/35.39 % SZS status Theorem for theBenchmark.p % 131.08/35.39 % SZS output start CNFRefutation for theBenchmark.p % 131.08/35.39 fof(reflexivity, axiom, ! [X0] : r1(X0,X0)). % 131.08/35.39 fof(transitivity, axiom, ! [X0] : ! [X1] : ! [X2] : (((r1(X0,X1) & r1(X1,X2)) => r1(X0,X2)))). % 131.08/35.39 fof(main, conjecture, ~? [X0] : ~((~! [X1] : ((~r1(X0,X1) | ~p4(X1))) | (~! [X1] : ((~r1(X0,X1) | ~((~! [X0] : ((~r1(X1,X0) | ~((~! [X1] : ((~r1(X0,X1) | ~((~! [X0] : ((~r1(X1,X0) | ~((~! [X1] : ((~r1(X0,X1) | ~((~! [X0] : ((~r1(X1,X0) | ~((~! [X1] : ((~r1(X0,X1) | ~((~! [X0] : ((~r1(X1,X0) | ~((~! [X1] : ((~r1(X0,X1) | ~((~! [X0] : ((~r1(X1,X0) | ~! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | p3(X0))) | ~p2(X1)))))) | ~! [X0] : ((~r1(X1,X0) | ~((~! [X1] : ((~r1(X0,X1) | ~((! [X0] : ((~r1(X1,X0) | p3(X0))) | ~p2(X1))))) & (p2(X0) & ~! [X1] : ((~r1(X0,X1) | ~! [X0] : ((~r1(X1,X0) | ~! [X1] : ((~r1(X0,X1) | ~p2(X1)))))))))))))))) | (~p1(X0) & (~! [X1] : ((~r1(X0,X1) | ~! [X0] : ((~r1(X1,X0) | p1(X0))))) & ! [X1] : ((~r1(X0,X1) | (p1(X1) | ~! [X0] : ((~r1(X1,X0) | ~((~! [X1] : ((~r1(X0,X1) | p1(X1))) & p1(X0)))))))))))))) | (~p1(X1) & (~! [X0] : ((~r1(X1,X0) | ~! [X1] : ((~r1(X0,X1) | p1(X1))))) & ! [X0] : ((~r1(X1,X0) | (p1(X0) | ~! [X1] : ((~r1(X0,X1) | ~((~! [X0] : ((~r1(X1,X0) | p1(X0))) & p1(X1)))))))))))))) | (~p1(X0) & (~! [X1] : ((~r1(X0,X1) | ~! [X0] : ((~r1(X1,X0) | p1(X0))))) & ! [X1] : ((~r1(X0,X1) | (p1(X1) | ~! [X0] : ((~r1(X1,X0) | ~((~! [X1] : ((~r1(X0,X1) | p1(X1))) & p1(X0)))))))))))))) | (~p1(X1) & (~! [X0] : ((~r1(X1,X0) | ~! [X1] : ((~r1(X0,X1) | p1(X1))))) & ! [X0] : ((~r1(X1,X0) | (p1(X0) | ~! [X1] : ((~r1(X0,X1) | ~((~! [X0] : ((~r1(X1,X0) | p1(X0))) & p1(X1)))))))))))))) | (~p1(X0) & (~! [X1] : ((~r1(X0,X1) | ~! [X0] : ((~r1(X1,X0) | p1(X0))))) & ! [X1] : ((~r1(X0,X1) | (p1(X1) | ~! [X0] : ((~r1(X1,X0) | ~((~! [X1] : ((~r1(X0,X1) | p1(X1))) & p1(X0)))))))))))))) | (~p1(X1) & (~! [X0] : ((~r1(X1,X0) | ~! [X1] : ((~r1(X0,X1) | p1(X1))))) & ! [X0] : ((~r1(X1,X0) | (p1(X0) | ~! [X1] : ((~r1(X0,X1) | ~((~! [X0] : ((~r1(X1,X0) | p1(X0))) & p1(X1)))))))))))))) | (~p1(X0) & (~! [X1] : ((~r1(X0,X1) | ~! [X0] : ((~r1(X1,X0) | p1(X0))))) & ! [X1] : ((~r1(X0,X1) | (p1(X1) | ~! [X0] : ((~r1(X1,X0) | ~((~! [X1] : ((~r1(X0,X1) | p1(X1))) & p1(X0)))))))))))))) | (~p1(X1) & (~! [X0] : ((~r1(X1,X0) | ~! [X1] : ((~r1(X0,X1) | p1(X1))))) & ! [X0] : ((~r1(X1,X0) | (p1(X0) | ~! [X1] : ((~r1(X0,X1) | ~((~! [X0] : ((~r1(X1,X0) | p1(X0))) & p1(X1)))))))))))))) | ((~p1(X0) & (~! [X1] : ((~r1(X0,X1) | ~! [X0] : ((~r1(X1,X0) | p1(X0))))) & ! [X1] : ((~r1(X0,X1) | (p1(X1) | ~! [X0] : ((~r1(X1,X0) | ~((~! [X1] : ((~r1(X0,X1) | p1(X1))) & p1(X0)))))))))) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | ~! [X1] : ((~r1(X0,X1) | p1(X1))))) | ! [X0] : ((~r1(X1,X0) | p1(X0)))))) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | ~! [X0] : ((~r1(X1,X0) | p1(X0))))) | ! [X1] : ((~r1(X0,X1) | p1(X1)))))) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | ~! [X1] : ((~r1(X0,X1) | p1(X1))))) | ! [X0] : ((~r1(X1,X0) | p1(X0)))))) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | ~! [X0] : ((~r1(X1,X0) | p1(X0))))) | ! [X1] : ((~r1(X0,X1) | p1(X1)))))) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | ~! [X1] : ((~r1(X0,X1) | p1(X1))))) | ! [X0] : ((~r1(X1,X0) | p1(X0)))))) | (! [X1] : ((~r1(X0,X1) | ~! [X0] : ((~r1(X1,X0) | ~! [X1] : ((~r1(X0,X1) | p2(X1))))))) | ~! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | ~p1(X1))))) | ~! [X0] : ((~r1(X1,X0) | ~p1(X0)))))))))) | ~! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | ~p1(X0))))) | ~! [X1] : ((~r1(X0,X1) | ~p1(X1)))))))))) | ~! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | ~p1(X1))))) | ~! [X0] : ((~r1(X1,X0) | ~p1(X0)))))))))) | ~! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | ~p1(X0))))) | ~! [X1] : ((~r1(X0,X1) | ~p1(X1)))))))))) | ~! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | ~p1(X1))))) | ~! [X0] : ((~r1(X1,X0) | ~p1(X0))))))))))))). % 131.08/35.39 fof(negated_conjecture, negated_conjecture, ~~? [X0] : ~((~! [X1] : ((~r1(X0,X1) | ~p4(X1))) | (~! [X1] : ((~r1(X0,X1) | ~((~! [X0] : ((~r1(X1,X0) | ~((~! [X1] : ((~r1(X0,X1) | ~((~! [X0] : ((~r1(X1,X0) | ~((~! [X1] : ((~r1(X0,X1) | ~((~! [X0] : ((~r1(X1,X0) | ~((~! [X1] : ((~r1(X0,X1) | ~((~! [X0] : ((~r1(X1,X0) | ~((~! [X1] : ((~r1(X0,X1) | ~((~! [X0] : ((~r1(X1,X0) | ~! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | p3(X0))) | ~p2(X1)))))) | ~! [X0] : ((~r1(X1,X0) | ~((~! [X1] : ((~r1(X0,X1) | ~((! [X0] : ((~r1(X1,X0) | p3(X0))) | ~p2(X1))))) & (p2(X0) & ~! [X1] : ((~r1(X0,X1) | ~! [X0] : ((~r1(X1,X0) | ~! [X1] : ((~r1(X0,X1) | ~p2(X1)))))))))))))))) | (~p1(X0) & (~! [X1] : ((~r1(X0,X1) | ~! [X0] : ((~r1(X1,X0) | p1(X0))))) & ! [X1] : ((~r1(X0,X1) | (p1(X1) | ~! [X0] : ((~r1(X1,X0) | ~((~! [X1] : ((~r1(X0,X1) | p1(X1))) & p1(X0)))))))))))))) | (~p1(X1) & (~! [X0] : ((~r1(X1,X0) | ~! [X1] : ((~r1(X0,X1) | p1(X1))))) & ! [X0] : ((~r1(X1,X0) | (p1(X0) | ~! [X1] : ((~r1(X0,X1) | ~((~! [X0] : ((~r1(X1,X0) | p1(X0))) & p1(X1)))))))))))))) | (~p1(X0) & (~! [X1] : ((~r1(X0,X1) | ~! [X0] : ((~r1(X1,X0) | p1(X0))))) & ! [X1] : ((~r1(X0,X1) | (p1(X1) | ~! [X0] : ((~r1(X1,X0) | ~((~! [X1] : ((~r1(X0,X1) | p1(X1))) & p1(X0)))))))))))))) | (~p1(X1) & (~! [X0] : ((~r1(X1,X0) | ~! [X1] : ((~r1(X0,X1) | p1(X1))))) & ! [X0] : ((~r1(X1,X0) | (p1(X0) | ~! [X1] : ((~r1(X0,X1) | ~((~! [X0] : ((~r1(X1,X0) | p1(X0))) & p1(X1)))))))))))))) | (~p1(X0) & (~! [X1] : ((~r1(X0,X1) | ~! [X0] : ((~r1(X1,X0) | p1(X0))))) & ! [X1] : ((~r1(X0,X1) | (p1(X1) | ~! [X0] : ((~r1(X1,X0) | ~((~! [X1] : ((~r1(X0,X1) | p1(X1))) & p1(X0)))))))))))))) | (~p1(X1) & (~! [X0] : ((~r1(X1,X0) | ~! [X1] : ((~r1(X0,X1) | p1(X1))))) & ! [X0] : ((~r1(X1,X0) | (p1(X0) | ~! [X1] : ((~r1(X0,X1) | ~((~! [X0] : ((~r1(X1,X0) | p1(X0))) & p1(X1)))))))))))))) | (~p1(X0) & (~! [X1] : ((~r1(X0,X1) | ~! [X0] : ((~r1(X1,X0) | p1(X0))))) & ! [X1] : ((~r1(X0,X1) | (p1(X1) | ~! [X0] : ((~r1(X1,X0) | ~((~! [X1] : ((~r1(X0,X1) | p1(X1))) & p1(X0)))))))))))))) | (~p1(X1) & (~! [X0] : ((~r1(X1,X0) | ~! [X1] : ((~r1(X0,X1) | p1(X1))))) & ! [X0] : ((~r1(X1,X0) | (p1(X0) | ~! [X1] : ((~r1(X0,X1) | ~((~! [X0] : ((~r1(X1,X0) | p1(X0))) & p1(X1)))))))))))))) | ((~p1(X0) & (~! [X1] : ((~r1(X0,X1) | ~! [X0] : ((~r1(X1,X0) | p1(X0))))) & ! [X1] : ((~r1(X0,X1) | (p1(X1) | ~! [X0] : ((~r1(X1,X0) | ~((~! [X1] : ((~r1(X0,X1) | p1(X1))) & p1(X0)))))))))) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | ~! [X1] : ((~r1(X0,X1) | p1(X1))))) | ! [X0] : ((~r1(X1,X0) | p1(X0)))))) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | ~! [X0] : ((~r1(X1,X0) | p1(X0))))) | ! [X1] : ((~r1(X0,X1) | p1(X1)))))) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | ~! [X1] : ((~r1(X0,X1) | p1(X1))))) | ! [X0] : ((~r1(X1,X0) | p1(X0)))))) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | ~! [X0] : ((~r1(X1,X0) | p1(X0))))) | ! [X1] : ((~r1(X0,X1) | p1(X1)))))) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | ~! [X1] : ((~r1(X0,X1) | p1(X1))))) | ! [X0] : ((~r1(X1,X0) | p1(X0)))))) | (! [X1] : ((~r1(X0,X1) | ~! [X0] : ((~r1(X1,X0) | ~! [X1] : ((~r1(X0,X1) | p2(X1))))))) | ~! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | ~p1(X1))))) | ~! [X0] : ((~r1(X1,X0) | ~p1(X0)))))))))) | ~! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | ~p1(X0))))) | ~! [X1] : ((~r1(X0,X1) | ~p1(X1)))))))))) | ~! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | ~p1(X1))))) | ~! [X0] : ((~r1(X1,X0) | ~p1(X0)))))))))) | ~! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | ~p1(X0))))) | ~! [X1] : ((~r1(X0,X1) | ~p1(X1)))))))))) | ~! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | ~p1(X1))))) | ~! [X0] : ((~r1(X1,X0) | ~p1(X0)))))))))))), inference(negate_conjecture, [status(cth)], [main])). % 131.08/35.39 cnf(c0, plain, r1(X0,X0), inference(clausification, [status(esa)], [reflexivity])). % 131.08/35.39 cnf(c1, plain, ~r1(X0,X1) | ~r1(X2,X0) | r1(X2,X1), inference(clausification, [status(esa)], [transitivity])). % 131.08/35.39 cnf(c5, plain, r1(sK19,sK23), inference(clausification, [status(esa)], [negated_conjecture])). % 131.08/35.39 cnf(c6, plain, r1(sK23,sK24), inference(clausification, [status(esa)], [negated_conjecture])). % 131.08/35.39 cnf(c7, plain, r1(sK24,sK25), inference(clausification, [status(esa)], [negated_conjecture])). % 131.08/35.39 cnf(c8, plain, r1(sK25,sK26), inference(clausification, [status(esa)], [negated_conjecture])). % 131.08/35.39 cnf(c9, plain, r1(sK26,sK27), inference(clausification, [status(esa)], [negated_conjecture])). % 131.08/35.39 cnf(c10, plain, ~r1(sK27,X0) | r1(X0,sK29(X0)), inference(clausification, [status(esa)], [negated_conjecture])). % 131.08/35.39 cnf(c11, plain, ~r1(sK27,X0) | ~p2(sK29(X0)), inference(clausification, [status(esa)], [negated_conjecture])). % 131.08/35.39 cnf(c47, plain, ~r1(sK19,X0) | X1(X0), inference(clausification, [status(esa)], [negated_conjecture])). % 131.08/35.39 cnf(c53, plain, ~X0(X1) | ~r1(X1,X2) | p2(X2), inference(clausification, [status(esa)], [negated_conjecture])). % 131.08/35.39 cnf(c54, plain, ~X0(X1) | ~r1(X1,X2) | r1(X2,sK77(X2)), inference(clausification, [status(esa)], [negated_conjecture])). % 131.08/35.39 cnf(c55, plain, ~X0(X1) | ~r1(X1,X2) | p2(sK77(X2)), inference(clausification, [status(esa)], [negated_conjecture])). % 131.08/35.39 cnf(c58, plain, ~r1(X0,X1) | r1(X2,sK81(X2)) | ~p2(X1) | ~X3(X0) | X4(X1) | ~r1(X1,X2), inference(clausification, [status(esa)], [negated_conjecture])). % 131.08/35.39 cnf(c59, plain, ~r1(X0,X1) | ~p2(X1) | ~p2(X2) | ~r1(sK81(X3),X2) | ~X4(X0) | X5(X1) | ~r1(X1,X3), inference(clausification, [status(esa)], [negated_conjecture])). % 131.08/35.39 cnf(c66, plain, ~X0(X1) | ~r1(X1,X2) | ~r1(X2,X3) | X4(X3), inference(clausification, [status(esa)], [negated_conjecture])). % 131.08/35.39 cnf(c77, plain, ~X0(X1) | ~r1(X1,X2) | ~r1(X2,X3) | X4(X3), inference(clausification, [status(esa)], [negated_conjecture])). % 131.08/35.39 cnf(c88, plain, ~X0(X1) | ~r1(X1,X2) | ~r1(X2,X3) | X4(X3), inference(clausification, [status(esa)], [negated_conjecture])). % 131.08/35.39 cnf(c99, plain, ~X0(X1) | ~r1(X1,X2) | ~r1(X2,X3) | X4(X3), inference(clausification, [status(esa)], [negated_conjecture])). % 131.08/35.39 cnf(d0, plain, ~r1(X0,X1) | ~r1(sK81(X1),X2) | ~p2(X2) | ~p2(X1) | 'Ts5'(X1) | ~'Ts6'(X0), inference(resolution, [status(thm)], [c59,c0])). % 131.08/35.39 cnf(d1, plain, r1(X0,sK27) | ~r1(X0,sK26), inference(resolution, [status(thm)], [c9,c1])). % 131.08/35.39 cnf(d2, plain, r1(sK25,sK27), inference(resolution, [status(thm)], [d1,c8])). % 131.08/35.39 cnf(d3, plain, r1(sK27,sK77(sK27)) | ~'Ts6'(sK25), inference(resolution, [status(thm)], [d2,c54])). % 131.08/35.39 cnf(d4, plain, ~r1(X0,X1) | 'Ts6'(X1) | ~'Ts9'(X0), inference(resolution, [status(thm)], [c66,c0])). % 131.08/35.39 cnf(d5, plain, 'Ts6'(X0) | ~'Ts9'(X0), inference(resolution, [status(thm)], [d4,c0])). % 131.08/35.39 cnf(d6, plain, ~r1(X0,X1) | 'Ts9'(X1) | ~'Ts12'(X0), inference(resolution, [status(thm)], [c77,c0])). % 131.08/35.39 cnf(d7, plain, 'Ts9'(X0) | ~'Ts12'(X0), inference(resolution, [status(thm)], [d6,c0])). % 131.08/35.39 cnf(d8, plain, ~r1(X0,X1) | 'Ts12'(X1) | ~'Ts15'(X0), inference(resolution, [status(thm)], [c88,c0])). % 131.08/35.39 cnf(d9, plain, 'Ts12'(sK25) | ~'Ts15'(sK24), inference(resolution, [status(thm)], [d8,c7])). % 131.08/35.39 cnf(d10, plain, r1(X0,sK24) | ~r1(X0,sK23), inference(resolution, [status(thm)], [c6,c1])). % 131.08/35.39 cnf(d11, plain, r1(sK19,sK24), inference(resolution, [status(thm)], [d10,c5])). % 131.08/35.39 cnf(d12, plain, 'Ts18'(sK24), inference(resolution, [status(thm)], [d11,c47])). % 131.08/35.39 cnf(d13, plain, ~r1(X0,X1) | ~'Ts18'(X0) | 'Ts15'(X1), inference(resolution, [status(thm)], [c99,c0])). % 131.08/35.39 cnf(d14, plain, ~'Ts18'(X0) | 'Ts15'(X0), inference(resolution, [status(thm)], [d13,c0])). % 131.08/35.39 cnf(d15, plain, 'Ts15'(sK24), inference(resolution, [status(thm)], [d14,d12])). % 131.08/35.39 cnf(d16, plain, 'Ts12'(sK25), inference(resolution, [status(thm)], [d15,d9])). % 131.08/35.39 cnf(d17, plain, 'Ts9'(sK25), inference(resolution, [status(thm)], [d16,d7])). % 131.08/35.39 cnf(d18, plain, 'Ts6'(sK25), inference(resolution, [status(thm)], [d17,d5])). % 131.08/35.39 cnf(d19, plain, r1(sK27,sK77(sK27)), inference(resolution, [status(thm)], [d18,d3])). % 131.08/35.39 cnf(d20, plain, ~r1(sK81(sK77(sK27)),X0) | ~p2(X0) | ~p2(sK77(sK27)) | 'Ts5'(sK77(sK27)) | ~'Ts6'(sK27), inference(resolution, [status(thm)], [d19,d0])). % 131.08/35.39 cnf(d21, plain, 'Ts12'(X0) | ~'Ts15'(X0), inference(resolution, [status(thm)], [d8,c0])). % 131.08/35.39 cnf(d22, plain, r1(X0,sK26) | ~r1(X0,sK25), inference(resolution, [status(thm)], [c8,c1])). % 131.08/35.39 cnf(d23, plain, r1(X0,sK25) | ~r1(X0,sK24), inference(resolution, [status(thm)], [c7,c1])). % 131.08/35.39 cnf(d24, plain, r1(sK19,sK25), inference(resolution, [status(thm)], [d11,d23])). % 131.08/35.39 cnf(d25, plain, r1(sK19,sK26), inference(resolution, [status(thm)], [d24,d22])). % 131.08/35.39 cnf(d26, plain, r1(sK19,sK27), inference(resolution, [status(thm)], [d25,d1])). % 131.08/35.39 cnf(d27, plain, 'Ts18'(sK27), inference(resolution, [status(thm)], [d26,c47])). % 131.08/35.39 cnf(d28, plain, 'Ts15'(sK27), inference(resolution, [status(thm)], [d14,d27])). % 131.08/35.39 cnf(d29, plain, 'Ts12'(sK27), inference(resolution, [status(thm)], [d28,d21])). % 131.08/35.39 cnf(d30, plain, 'Ts9'(sK27), inference(resolution, [status(thm)], [d29,d7])). % 131.08/35.39 cnf(d31, plain, 'Ts6'(sK27), inference(resolution, [status(thm)], [d30,d5])). % 131.08/35.39 cnf(d32, plain, ~r1(sK81(sK77(sK27)),X0) | ~p2(X0) | ~p2(sK77(sK27)) | 'Ts5'(sK77(sK27)), inference(resolution, [status(thm)], [d31,d20])). % 131.08/35.39 cnf(d33, plain, p2(sK77(X0)) | ~'Ts6'(X0), inference(resolution, [status(thm)], [c55,c0])). % 131.08/35.39 cnf(d34, plain, p2(sK77(sK27)), inference(resolution, [status(thm)], [d31,d33])). % 131.08/35.39 cnf(d35, plain, ~r1(sK81(sK77(sK27)),X0) | ~p2(X0) | 'Ts5'(sK77(sK27)), inference(resolution, [status(thm)], [d34,d32])). % 131.08/35.39 cnf(d36, plain, r1(sK77(sK27),sK29(sK77(sK27))), inference(resolution, [status(thm)], [d19,c10])). % 131.08/35.39 cnf(d37, plain, p2(sK29(sK77(sK27))) | ~'Ts5'(sK77(sK27)), inference(resolution, [status(thm)], [d36,c53])). % 131.08/35.39 cnf(d38, plain, ~p2(sK29(sK77(sK27))), inference(resolution, [status(thm)], [d19,c11])). % 131.08/35.39 cnf(d39, plain, ~'Ts5'(sK77(sK27)), inference(resolution, [status(thm)], [d38,d37])). % 131.08/35.39 cnf(d40, plain, ~r1(sK81(sK77(sK27)),X0) | ~p2(X0), inference(resolution, [status(thm)], [d39,d35])). % 131.08/35.39 cnf(d41, plain, r1(X0,sK77(X0)) | ~'Ts6'(X0), inference(resolution, [status(thm)], [c54,c0])). % 131.08/35.39 cnf(d42, plain, ~r1(sK77(sK27),X0) | 'Ts12'(X0) | ~'Ts15'(sK27), inference(resolution, [status(thm)], [d19,c88])). % 131.08/35.39 cnf(d43, plain, ~r1(sK77(sK27),X0) | 'Ts12'(X0), inference(resolution, [status(thm)], [d28,d42])). % 131.08/35.39 cnf(d44, plain, r1(X0,sK81(X0)) | ~r1(sK77(sK27),X0) | ~p2(sK77(sK27)) | 'Ts5'(sK77(sK27)) | ~'Ts6'(sK27), inference(resolution, [status(thm)], [d19,c58])). % 131.08/35.39 cnf(d45, plain, r1(X0,sK81(X0)) | ~r1(sK77(sK27),X0) | ~p2(sK77(sK27)) | 'Ts5'(sK77(sK27)), inference(resolution, [status(thm)], [d31,d44])). % 131.08/35.39 cnf(d46, plain, r1(X0,sK81(X0)) | ~r1(sK77(sK27),X0) | 'Ts5'(sK77(sK27)), inference(resolution, [status(thm)], [d34,d45])). % 131.08/35.39 cnf(d47, plain, r1(X0,sK81(X0)) | ~r1(sK77(sK27),X0), inference(resolution, [status(thm)], [d39,d46])). % 131.08/35.39 cnf(d48, plain, r1(sK77(sK27),sK81(sK77(sK27))), inference(resolution, [status(thm)], [d47,c0])). % 131.08/35.39 cnf(d49, plain, 'Ts12'(sK81(sK77(sK27))), inference(resolution, [status(thm)], [d48,d43])). % 131.08/35.39 cnf(d50, plain, 'Ts9'(sK81(sK77(sK27))), inference(resolution, [status(thm)], [d49,d7])). % 131.08/35.39 cnf(d51, plain, 'Ts6'(sK81(sK77(sK27))), inference(resolution, [status(thm)], [d50,d5])). % 131.08/35.39 cnf(d52, plain, r1(sK81(sK77(sK27)),sK77(sK81(sK77(sK27)))), inference(resolution, [status(thm)], [d51,d41])). % 131.08/35.39 cnf(d53, plain, ~p2(sK77(sK81(sK77(sK27)))), inference(resolution, [status(thm)], [d52,d40])). % 131.08/35.39 cnf(d54, plain, p2(sK77(sK81(sK77(sK27)))), inference(resolution, [status(thm)], [d51,d33])). % 131.08/35.39 cnf(d55, plain, $false, inference(resolution, [status(thm)], [d54,d53])). % 131.08/35.39 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------