%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : PUZ075+1 : TPTP v9.3.1. Released v3.5.0. % Transfm : none % Format : tptp:raw % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % Computer : n005.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:22:14 AM UTC 2026 % Result : Theorem 33.46s 5.03s % Output : CNFRefutation 33.46s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : PUZ075+1 : TPTP v9.3.1. Released v3.5.0. % 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.08/0.36 % Computer : n005.cluster.edu % 0.08/0.36 % Model : x86_64 x86_64 % 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.36 % Memory : 8046.5625MB % 0.08/0.36 % OS : Linux 6.8.0-71-generic % 0.08/0.36 % CPULimit : 300 % 0.08/0.36 % WCLimit : 300 % 0.08/0.36 % DateTime : Sat Sep 26 05:14:17 UTC 2026 % 0.08/0.36 % CPUTime : % 0.08/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 33.46/5.03 % SZS status Theorem for theBenchmark.p % 33.46/5.03 % SZS output start CNFRefutation for theBenchmark.p % 33.46/5.03 fof(tlhfof24987, axiom, ! [X0] : ! [X1] : ((edge(X1,X0) <=> ((X1 = cell1 & X0 = cell2) | ((X1 = cell2 & X0 = cell3) | ((X1 = cell3 & X0 = cell4) | ((X1 = cell4 & X0 = cell5) | ((X1 = cell5 & X0 = cell6) | ((X1 = cell6 & X0 = cell7) | ((X1 = cell7 & X0 = cell8) | ((X1 = cell8 & X0 = cell9) | ((X1 = cell9 & X0 = cell10) | ((X1 = cell11 & X0 = cell12) | ((X1 = cell12 & X0 = cell13) | ((X1 = cell13 & X0 = cell14) | ((X1 = cell14 & X0 = cell15) | ((X1 = cell15 & X0 = cell16) | ((X1 = cell16 & X0 = cell17) | ((X1 = cell17 & X0 = cell18) | ((X1 = cell18 & X0 = cell19) | ((X1 = cell19 & X0 = cell20) | ((X1 = cell21 & X0 = cell22) | ((X1 = cell22 & X0 = cell23) | ((X1 = cell23 & X0 = cell24) | ((X1 = cell24 & X0 = cell25) | ((X1 = cell25 & X0 = cell26) | ((X1 = cell26 & X0 = cell27) | ((X1 = cell27 & X0 = cell28) | ((X1 = cell28 & X0 = cell29) | ((X1 = cell29 & X0 = cell30) | ((X1 = cell31 & X0 = cell32) | ((X1 = cell32 & X0 = cell33) | ((X1 = cell33 & X0 = cell34) | ((X1 = cell34 & X0 = cell35) | ((X1 = cell35 & X0 = cell36) | ((X1 = cell36 & X0 = cell37) | ((X1 = cell37 & X0 = cell38) | ((X1 = cell38 & X0 = cell39) | ((X1 = cell39 & X0 = cell40) | ((X1 = cell41 & X0 = cell42) | ((X1 = cell42 & X0 = cell43) | ((X1 = cell43 & X0 = cell44) | ((X1 = cell44 & X0 = cell45) | ((X1 = cell45 & X0 = cell46) | ((X1 = cell46 & X0 = cell47) | ((X1 = cell47 & X0 = cell48) | ((X1 = cell48 & X0 = cell49) | ((X1 = cell49 & X0 = cell50) | ((X1 = cell51 & X0 = cell52) | ((X1 = cell52 & X0 = cell53) | ((X1 = cell53 & X0 = cell54) | ((X1 = cell54 & X0 = cell55) | ((X1 = cell55 & X0 = cell56) | ((X1 = cell56 & X0 = cell57) | ((X1 = cell57 & X0 = cell58) | ((X1 = cell58 & X0 = cell59) | ((X1 = cell59 & X0 = cell60) | ((X1 = cell61 & X0 = cell62) | ((X1 = cell62 & X0 = cell63) | ((X1 = cell63 & X0 = cell64) | ((X1 = cell64 & X0 = cell65) | ((X1 = cell65 & X0 = cell66) | ((X1 = cell66 & X0 = cell67) | ((X1 = cell67 & X0 = cell68) | ((X1 = cell68 & X0 = cell69) | ((X1 = cell69 & X0 = cell70) | ((X1 = cell71 & X0 = cell72) | ((X1 = cell72 & X0 = cell73) | ((X1 = cell73 & X0 = cell74) | ((X1 = cell74 & X0 = cell75) | ((X1 = cell75 & X0 = cell76) | ((X1 = cell76 & X0 = cell77) | ((X1 = cell77 & X0 = cell78) | ((X1 = cell78 & X0 = cell79) | ((X1 = cell79 & X0 = cell80) | ((X1 = cell81 & X0 = cell82) | ((X1 = cell82 & X0 = cell83) | ((X1 = cell83 & X0 = cell84) | ((X1 = cell84 & X0 = cell85) | ((X1 = cell85 & X0 = cell86) | ((X1 = cell86 & X0 = cell87) | ((X1 = cell87 & X0 = cell88) | ((X1 = cell88 & X0 = cell89) | ((X1 = cell89 & X0 = cell90) | ((X1 = cell91 & X0 = cell92) | ((X1 = cell92 & X0 = cell93) | ((X1 = cell93 & X0 = cell94) | ((X1 = cell94 & X0 = cell95) | ((X1 = cell95 & X0 = cell96) | ((X1 = cell96 & X0 = cell97) | ((X1 = cell97 & X0 = cell98) | ((X1 = cell98 & X0 = cell99) | ((X1 = cell99 & X0 = cell100) | ((X1 = cell1 & X0 = cell11) | ((X1 = cell2 & X0 = cell12) | ((X1 = cell3 & X0 = cell13) | ((X1 = cell4 & X0 = cell14) | ((X1 = cell5 & X0 = cell15) | ((X1 = cell6 & X0 = cell16) | ((X1 = cell7 & X0 = cell17) | ((X1 = cell8 & X0 = cell18) | ((X1 = cell9 & X0 = cell19) | ((X1 = cell10 & X0 = cell20) | ((X1 = cell11 & X0 = cell21) | ((X1 = cell12 & X0 = cell22) | ((X1 = cell13 & X0 = cell23) | ((X1 = cell14 & X0 = cell24) | ((X1 = cell15 & X0 = cell25) | ((X1 = cell16 & X0 = cell26) | ((X1 = cell17 & X0 = cell27) | ((X1 = cell18 & X0 = cell28) | ((X1 = cell19 & X0 = cell29) | ((X1 = cell20 & X0 = cell30) | ((X1 = cell21 & X0 = cell31) | ((X1 = cell22 & X0 = cell32) | ((X1 = cell23 & X0 = cell33) | ((X1 = cell24 & X0 = cell34) | ((X1 = cell25 & X0 = cell35) | ((X1 = cell26 & X0 = cell36) | ((X1 = cell27 & X0 = cell37) | ((X1 = cell28 & X0 = cell38) | ((X1 = cell29 & X0 = cell39) | ((X1 = cell30 & X0 = cell40) | ((X1 = cell31 & X0 = cell41) | ((X1 = cell32 & X0 = cell42) | ((X1 = cell33 & X0 = cell43) | ((X1 = cell34 & X0 = cell44) | ((X1 = cell35 & X0 = cell45) | ((X1 = cell36 & X0 = cell46) | ((X1 = cell37 & X0 = cell47) | ((X1 = cell38 & X0 = cell48) | ((X1 = cell39 & X0 = cell49) | ((X1 = cell40 & X0 = cell50) | ((X1 = cell41 & X0 = cell51) | ((X1 = cell42 & X0 = cell52) | ((X1 = cell43 & X0 = cell53) | ((X1 = cell44 & X0 = cell54) | ((X1 = cell45 & X0 = cell55) | ((X1 = cell46 & X0 = cell56) | ((X1 = cell47 & X0 = cell57) | ((X1 = cell48 & X0 = cell58) | ((X1 = cell49 & X0 = cell59) | ((X1 = cell50 & X0 = cell60) | ((X1 = cell51 & X0 = cell61) | ((X1 = cell52 & X0 = cell62) | ((X1 = cell53 & X0 = cell63) | ((X1 = cell54 & X0 = cell64) | ((X1 = cell55 & X0 = cell65) | ((X1 = cell56 & X0 = cell66) | ((X1 = cell57 & X0 = cell67) | ((X1 = cell58 & X0 = cell68) | ((X1 = cell59 & X0 = cell69) | ((X1 = cell60 & X0 = cell70) | ((X1 = cell61 & X0 = cell71) | ((X1 = cell62 & X0 = cell72) | ((X1 = cell63 & X0 = cell73) | ((X1 = cell64 & X0 = cell74) | ((X1 = cell65 & X0 = cell75) | ((X1 = cell66 & X0 = cell76) | ((X1 = cell67 & X0 = cell77) | ((X1 = cell68 & X0 = cell78) | ((X1 = cell69 & X0 = cell79) | ((X1 = cell70 & X0 = cell80) | ((X1 = cell71 & X0 = cell81) | ((X1 = cell72 & X0 = cell82) | ((X1 = cell73 & X0 = cell83) | ((X1 = cell74 & X0 = cell84) | ((X1 = cell75 & X0 = cell85) | ((X1 = cell76 & X0 = cell86) | ((X1 = cell77 & X0 = cell87) | ((X1 = cell78 & X0 = cell88) | ((X1 = cell79 & X0 = cell89) | ((X1 = cell80 & X0 = cell90) | ((X1 = cell81 & X0 = cell91) | ((X1 = cell82 & X0 = cell92) | ((X1 = cell83 & X0 = cell93) | ((X1 = cell84 & X0 = cell94) | ((X1 = cell85 & X0 = cell95) | ((X1 = cell86 & X0 = cell96) | ((X1 = cell87 & X0 = cell97) | ((X1 = cell88 & X0 = cell98) | ((X1 = cell89 & X0 = cell99) | (X1 = cell90 & X0 = cell100))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))). % 33.46/5.03 fof(tlhfof24988, axiom, ! [X0] : ! [X1] : ((adj(X1,X0) <=> (edge(X1,X0) | edge(X0,X1))))). % 33.46/5.03 fof(tlhfof24989, conjecture, adj(cell12,cell13)). % 33.46/5.03 fof(negated_conjecture, negated_conjecture, ~adj(cell12,cell13), inference(negate_conjecture, [status(cth)], [tlhfof24989])). % 33.46/5.03 cnf(c1, plain, edge(X0,X1) | ~X2(X1,X0), inference(clausification, [status(esa)], [tlhfof24987])). % 33.46/5.03 cnf(c593, plain, X0(X1,X2) | X2 != cell12 | X1 != cell13, inference(clausification, [status(esa)], [tlhfof24987])). % 33.46/5.03 cnf(c602, plain, X0(X1,X2) | ~X3(X1,X2), inference(clausification, [status(esa)], [tlhfof24987])). % 33.46/5.03 cnf(c609, plain, X0(X1,X2) | ~X3(X1,X2), inference(clausification, [status(esa)], [tlhfof24987])). % 33.46/5.03 cnf(c616, plain, X0(X1,X2) | ~X3(X1,X2), inference(clausification, [status(esa)], [tlhfof24987])). % 33.46/5.03 cnf(c623, plain, X0(X1,X2) | ~X3(X1,X2), inference(clausification, [status(esa)], [tlhfof24987])). % 33.46/5.03 cnf(c630, plain, X0(X1,X2) | ~X3(X1,X2), inference(clausification, [status(esa)], [tlhfof24987])). % 33.46/5.03 cnf(c632, plain, adj(X0,X1) | ~edge(X0,X1), inference(clausification, [status(esa)], [tlhfof24988])). % 33.46/5.03 cnf(c634, plain, ~adj(cell12,cell13), inference(clausification, [status(esa)], [negated_conjecture])). % 33.46/5.03 cnf(d0, plain, X0 != cell12 | 'Ts84'(cell13,X0), inference(equality_resolution, [status(thm)], [c593])). % 33.46/5.03 cnf(d1, plain, 'Ts84'(cell13,cell12), inference(equality_resolution, [status(thm)], [d0])). % 33.46/5.03 cnf(d2, plain, 'Ts85'(cell13,cell12), inference(resolution, [status(thm)], [d1,c602])). % 33.46/5.03 cnf(d3, plain, 'Ts86'(cell13,cell12), inference(resolution, [status(thm)], [d2,c609])). % 33.46/5.03 cnf(d4, plain, 'Ts87'(cell13,cell12), inference(resolution, [status(thm)], [d3,c616])). % 33.46/5.03 cnf(d5, plain, 'Ts88'(cell13,cell12), inference(resolution, [status(thm)], [d4,c623])). % 33.46/5.03 cnf(d6, plain, 'Ts89'(cell13,cell12), inference(resolution, [status(thm)], [d5,c630])). % 33.46/5.03 cnf(d7, plain, edge(cell12,cell13), inference(resolution, [status(thm)], [d6,c1])). % 33.46/5.03 cnf(d8, plain, adj(cell12,cell13), inference(resolution, [status(thm)], [d7,c632])). % 33.46/5.03 cnf(d9, plain, $false, inference(resolution, [status(thm)], [c634,d8])). % 33.46/5.03 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------