%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : SET804+4 : TPTP v9.3.1. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % Computer : n016.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 08:33:15 AM UTC 2026 % Result : Theorem 4.06s 3.40s % Output : CNFRefutation 4.06s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.05 % Problem : SET804+4 : TPTP v9.3.1. Released v3.2.0. % 0.00/0.06 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.16/0.43 % Computer : n016.cluster.edu % 0.16/0.43 % Model : x86_64 x86_64 % 0.16/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.43 % Memory : 8046.5625MB % 0.16/0.43 % OS : Linux 6.8.0-71-generic % 0.16/0.43 % CPULimit : 300 % 0.16/0.44 % WCLimit : 300 % 0.16/0.44 % DateTime : Sat Sep 26 08:22:02 UTC 2026 % 0.16/0.44 % CPUTime : % 0.16/0.44 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 4.06/3.40 % SZS status Theorem for theBenchmark.p % 4.06/3.40 % SZS output start CNFRefutation for theBenchmark.p % 4.06/3.40 fof(least, axiom, ! [X0] : ! [X1] : ! [X2] : ((least(X2,X0,X1) <=> (member(X2,X1) & ! [X3] : ((member(X3,X1) => apply(X0,X2,X3))))))). % 4.06/3.40 fof(min, axiom, ! [X0] : ! [X1] : ! [X2] : ((min(X2,X0,X1) <=> (member(X2,X1) & ! [X3] : (((member(X3,X1) & apply(X0,X3,X2)) => X2 = X3)))))). % 4.06/3.40 fof(thIV16, conjecture, ! [X0] : ! [X1] : ((order(X0,X1) => ! [X2] : ! [X3] : (((min(X2,X0,X1) & (min(X3,X0,X1) & X2 != X3)) => ~? [X4] : least(X4,X0,X1)))))). % 4.06/3.40 fof(negated_conjecture, negated_conjecture, ~! [X0] : ! [X1] : ((order(X0,X1) => ! [X2] : ! [X3] : (((min(X2,X0,X1) & (min(X3,X0,X1) & X2 != X3)) => ~? [X4] : least(X4,X0,X1))))), inference(negate_conjecture, [status(cth)], [thIV16])). % 4.06/3.40 cnf(c38, plain, ~least(X0,X1,X2) | member(X0,X2), inference(clausification, [status(esa)], [least])). % 4.06/3.40 cnf(c39, plain, ~least(X0,X1,X2) | ~member(X3,X2) | apply(X1,X0,X3), inference(clausification, [status(esa)], [least])). % 4.06/3.40 cnf(c49, plain, ~min(X0,X1,X2) | X3(X2,X0,X1), inference(clausification, [status(esa)], [min])). % 4.06/3.40 cnf(c51, plain, ~X0(X1,X2,X3) | member(X2,X1), inference(clausification, [status(esa)], [min])). % 4.06/3.40 cnf(c52, plain, ~X0(X1,X2,X3) | ~member(X4,X1) | ~apply(X3,X4,X2) | X2 = X4, inference(clausification, [status(esa)], [min])). % 4.06/3.40 cnf(c73, plain, min(sK72,sK70,sK71), inference(clausification, [status(esa)], [negated_conjecture])). % 4.06/3.40 cnf(c74, plain, min(sK73,sK70,sK71), inference(clausification, [status(esa)], [negated_conjecture])). % 4.06/3.40 cnf(c75, plain, sK72 != sK73, inference(clausification, [status(esa)], [negated_conjecture])). % 4.06/3.40 cnf(c76, plain, least(sK74,sK70,sK71), inference(clausification, [status(esa)], [negated_conjecture])). % 4.06/3.40 cnf(d0, plain, ~member(X0,sK71) | apply(sK70,sK74,X0), inference(resolution, [status(thm)], [c39,c76])). % 4.06/3.40 cnf(d1, plain, 'Ts50'(sK71,sK72,sK70), inference(resolution, [status(thm)], [c49,c73])). % 4.06/3.40 cnf(d2, plain, sK72 = X0 | ~member(X0,sK71) | ~apply(sK70,X0,sK72), inference(resolution, [status(thm)], [c52,d1])). % 4.06/3.40 cnf(d3, plain, sK72 = sK74 | ~member(sK74,sK71) | ~member(sK72,sK71), inference(resolution, [status(thm)], [d2,d0])). % 4.06/3.40 cnf(d4, plain, member(sK74,sK71), inference(resolution, [status(thm)], [c38,c76])). % 4.06/3.40 cnf(d5, plain, sK72 = sK74 | ~member(sK72,sK71), inference(resolution, [status(thm)], [d4,d3])). % 4.06/3.40 cnf(d6, plain, member(sK72,sK71), inference(resolution, [status(thm)], [d1,c51])). % 4.06/3.40 cnf(d7, plain, sK72 = sK74, inference(resolution, [status(thm)], [d6,d5])). % 4.06/3.40 cnf(d8, plain, ~member(X0,sK71) | apply(sK70,sK72,X0), inference(demodulation, [status(thm)], [d0,d7])). % 4.06/3.40 cnf(d9, plain, 'Ts50'(sK71,sK73,sK70), inference(resolution, [status(thm)], [c49,c74])). % 4.06/3.40 cnf(d10, plain, sK73 = X0 | ~member(X0,sK71) | ~apply(sK70,X0,sK73), inference(resolution, [status(thm)], [c52,d9])). % 4.06/3.40 cnf(d11, plain, sK73 = sK72 | ~member(sK72,sK71) | ~member(sK73,sK71), inference(resolution, [status(thm)], [d10,d8])). % 4.06/3.40 cnf(d12, plain, member(sK73,sK71), inference(resolution, [status(thm)], [d9,c51])). % 4.06/3.40 cnf(d13, plain, sK73 = sK72 | ~member(sK72,sK71), inference(resolution, [status(thm)], [d12,d11])). % 4.06/3.40 cnf(d14, plain, sK73 = sK72, inference(resolution, [status(thm)], [d6,d13])). % 4.06/3.40 cnf(d15, plain, sK72 != sK72, inference(demodulation, [status(thm)], [c75,d14])). % 4.06/3.40 cnf(d16, plain, $false, inference(equality_resolution, [status(thm)], [d15])). % 4.06/3.40 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------