%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN332-1 : TPTP v8.2.0. Released v1.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n021.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Jun 24 19:05:12 EDT 2024 % Result : Unsatisfiable 1.05s 1.14s % Output : CNFRefutation 1.05s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SYN332-1 : TPTP v8.2.0. Released v1.2.0. % 0.11/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.32 % Computer : n021.cluster.edu % 0.12/0.32 % Model : x86_64 x86_64 % 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.32 % Memory : 8042.1875MB % 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.32 % CPULimit : 300 % 0.12/0.32 % WCLimit : 300 % 0.12/0.32 % DateTime : Sun Jun 23 22:09:24 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.56 start to proof:theBenchmark % 1.05/1.13 %------------------------------------------- % 1.05/1.13 % File :CSE---1.7 % 1.05/1.13 % Problem :theBenchmark % 1.05/1.13 % Transform :cnf % 1.05/1.13 % Format :tptp:raw % 1.05/1.13 % Command :java -jar mcs_scs.jar %d %s % 1.05/1.13 % 1.05/1.13 % Result :Theorem 0.530000s % 1.05/1.13 % Output :CNFRefutation 0.530000s % 1.05/1.13 %------------------------------------------- % 1.05/1.14 %-------------------------------------------------------------------------- % 1.05/1.14 % File : SYN332-1 : TPTP v8.2.0. Released v1.2.0. % 1.05/1.14 % Domain : Syntactic % 1.05/1.14 % Problem : Church problem 46.14 (4) % 1.05/1.14 % Version : Especial. % 1.05/1.14 % English : % 1.05/1.14 % 1.05/1.14 % Refs : [Chu56] Church (1956), Introduction to Mathematical Logic I % 1.05/1.14 % : [FL+93] Fermuller et al. (1993), Resolution Methods for the De % 1.05/1.14 % : [Tam94] Tammet (1994), Email to Geoff Sutcliffe. % 1.05/1.14 % Source : [Tam94] % 1.05/1.14 % Names : Ch14N4 [Tam94] % 1.05/1.14 % 1.05/1.14 % Status : Unsatisfiable % 1.05/1.14 % Rating : 0.00 v6.3.0, 0.14 v6.2.0, 0.00 v5.0.0, 0.07 v4.1.0, 0.00 v2.5.0, 0.20 v2.4.0, 0.00 v2.1.0, 0.00 v2.0.0 % 1.05/1.14 % Syntax : Number of clauses : 14 ( 0 unt; 6 nHn; 11 RR) % 1.05/1.14 % Number of literals : 34 ( 0 equ; 16 neg) % 1.05/1.14 % Maximal clause size : 3 ( 2 avg) % 1.05/1.14 % Maximal term depth : 2 ( 1 avg) % 1.05/1.14 % Number of predicates : 1 ( 1 usr; 0 prp; 2-2 aty) % 1.05/1.14 % Number of functors : 1 ( 1 usr; 0 con; 2-2 aty) % 1.05/1.14 % Number of variables : 28 ( 0 sgn) % 1.05/1.14 % SPC : CNF_UNS_RFO_NEQ_NHN % 1.05/1.14 % 1.05/1.14 % Comments : All the problems here can be decided by using a certain % 1.05/1.14 % completeness-preserving term ordering strategies. See [FL+93]. % 1.05/1.14 % : The conversion from the full 1st order form in [Chu56] % 1.05/1.14 % to clause form was done by hand by Tanel Tammet. % 1.05/1.14 %-------------------------------------------------------------------------- % 1.05/1.14 cnf(clause1,negated_conjecture, % 1.05/1.14 ( f(X,Y) % 1.05/1.14 | f(X,z(X,Y)) ) ). % 1.05/1.14 % 1.05/1.14 cnf(clause2,negated_conjecture, % 1.05/1.14 ( f(Y,X) % 1.05/1.14 | f(X,z(X,Y)) ) ). % 1.05/1.14 % 1.05/1.14 cnf(clause3,negated_conjecture, % 1.05/1.14 ( ~ f(X,Y) % 1.05/1.14 | ~ f(Y,X) % 1.05/1.14 | ~ f(X,z(X,Y)) ) ). % 1.05/1.14 % 1.05/1.14 cnf(clause4,negated_conjecture, % 1.05/1.14 ( f(X,z(X,Y)) % 1.05/1.14 | ~ f(z(X,Y),X) ) ). % 1.05/1.14 % 1.05/1.14 cnf(clause5,negated_conjecture, % 1.05/1.14 ( ~ f(X,z(X,Y)) % 1.05/1.14 | f(z(X,Y),X) ) ). % 1.05/1.14 % 1.05/1.14 cnf(clause6,negated_conjecture, % 1.05/1.14 ( f(X,z(X,Y)) % 1.05/1.14 | ~ f(Y,z(X,Y)) ) ). % 1.05/1.14 % 1.05/1.14 cnf(clause7,negated_conjecture, % 1.05/1.14 ( ~ f(X,z(X,Y)) % 1.05/1.14 | f(Y,z(X,Y)) ) ). % 1.05/1.14 % 1.05/1.14 cnf(clause8,negated_conjecture, % 1.05/1.14 ( ~ f(Y,X) % 1.05/1.14 | f(X,Y) % 1.05/1.14 | ~ f(z(X,Y),z(X,Y)) ) ). % 1.05/1.14 % 1.05/1.14 cnf(clause9,negated_conjecture, % 1.05/1.14 ( f(Y,X) % 1.05/1.14 | f(z(X,Y),z(X,Y)) ) ). % 1.05/1.14 % 1.05/1.14 cnf(clause10,negated_conjecture, % 1.05/1.14 ( ~ f(X,Y) % 1.05/1.14 | f(z(X,Y),z(X,Y)) ) ). % 1.05/1.14 % 1.05/1.14 cnf(clause11,negated_conjecture, % 1.05/1.14 ( f(X,Y) % 1.05/1.14 | ~ f(Y,X) % 1.05/1.14 | f(z(X,Y),Y) ) ). % 1.05/1.14 % 1.05/1.14 cnf(clause12,negated_conjecture, % 1.05/1.14 ( ~ f(X,Y) % 1.05/1.14 | f(Y,X) % 1.05/1.14 | f(z(X,Y),Y) ) ). % 1.05/1.14 % 1.05/1.14 cnf(clause13,negated_conjecture, % 1.05/1.14 ( f(X,Y) % 1.05/1.14 | f(Y,X) % 1.05/1.14 | ~ f(z(X,Y),Y) ) ). % 1.05/1.14 % 1.05/1.14 cnf(clause14,negated_conjecture, % 1.05/1.14 ( ~ f(X,Y) % 1.05/1.14 | ~ f(Y,X) % 1.05/1.14 | ~ f(z(X,Y),Y) ) ). % 1.05/1.14 % 1.05/1.14 %-------------------------------------------------------------------------- % 1.05/1.14 %------------------------------------------- % 1.05/1.14 % Proof found % 1.05/1.14 % SZS status Theorem for theBenchmark % 1.05/1.14 % SZS output start Proof % 1.05/1.14 %ClaNum:14(EqnAxiom:0) % 1.05/1.14 %VarNum:89(SingletonVarNum:28) % 1.05/1.14 %MaxLitNum:3 % 1.05/1.14 %MaxfuncDepth:1 % 1.05/1.14 %SharedTerms:0 % 1.05/1.14 %goalClause: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 % 1.05/1.14 [1]P1(x11,x12)+P1(x12,f1(x12,x11)) % 1.05/1.14 [2]P1(x21,x22)+P1(x21,f1(x21,x22)) % 1.05/1.14 [5]P1(x51,x52)+P1(f1(x52,x51),f1(x52,x51)) % 1.05/1.14 [6]~P1(x61,x62)+P1(f1(x61,x62),f1(x61,x62)) % 1.05/1.14 [8]P1(x81,f1(x82,x81))+~P1(x82,f1(x82,x81)) % 1.05/1.14 [9]P1(x91,f1(x91,x92))+~P1(x92,f1(x91,x92)) % 1.05/1.14 [10]P1(x101,f1(x101,x102))+~P1(f1(x101,x102),x101) % 1.05/1.14 [11]P1(f1(x111,x112),x111)+~P1(x111,f1(x111,x112)) % 1.05/1.14 [3]~P1(x32,x31)+P1(x31,x32)+P1(f1(x32,x31),x31) % 1.05/1.14 [4]~P1(x42,x41)+P1(x41,x42)+P1(f1(x41,x42),x42) % 1.05/1.14 [7]P1(x72,x71)+P1(x71,x72)+~P1(f1(x72,x71),x71) % 1.05/1.14 [12]~P1(x122,x121)+~P1(x121,x122)+~P1(x122,f1(x122,x121)) % 1.05/1.14 [13]~P1(x132,x131)+~P1(x131,x132)+~P1(f1(x132,x131),x131) % 1.05/1.14 [14]~P1(x142,x141)+P1(x141,x142)+~P1(f1(x141,x142),f1(x141,x142)) % 1.05/1.14 %EqnAxiom % 1.05/1.14 % 1.05/1.14 %------------------------------------------- % 1.05/1.14 cnf(25,plain, % 1.05/1.14 (~P1(x251,x252)+~P1(f1(x252,x251),f1(x252,x251))+~P1(x252,f1(x252,x251))), % 1.05/1.14 inference(scs_inference,[],[14,12])). % 1.05/1.14 cnf(40,plain, % 1.05/1.14 (P1(x401,x402)+P1(f1(x402,x401),x402)), % 1.05/1.14 inference(scs_inference,[],[1,11])). % 1.05/1.14 cnf(52,plain, % 1.05/1.14 (~P1(x521,f1(x521,x522))+~P1(x522,x521)+P1(f1(x521,x522),f1(f1(x521,x522),f1(x521,x522)))), % 1.05/1.14 inference(scs_inference,[],[1,25])). % 1.05/1.14 cnf(56,plain, % 1.05/1.14 (~P1(x561,x562)+P1(f1(x562,x561),f1(f1(x562,x561),f1(x562,x561)))+P1(f1(x562,x561),f1(f1(x562,x561),x562))), % 1.05/1.14 inference(scs_inference,[],[1,52])). % 1.05/1.14 cnf(57,plain, % 1.05/1.14 (P1(f1(x571,x572),f1(f1(x571,x572),x571))+~P1(f1(x571,x572),f1(x571,x572))+~P1(x572,x571)), % 1.05/1.14 inference(scs_inference,[],[56,12])). % 1.05/1.14 cnf(79,plain, % 1.05/1.15 (~P1(x791,x792)+P1(f1(x792,x791),f1(f1(x792,x791),f1(x792,x791)))+P1(x792,f1(x792,f1(x792,x791)))), % 1.05/1.15 inference(scs_inference,[],[2,52])). % 1.05/1.15 cnf(80,plain, % 1.05/1.15 (P1(x801,f1(x801,f1(x801,x802)))+~P1(f1(x801,x802),f1(x801,x802))+~P1(x802,x801)), % 1.05/1.15 inference(scs_inference,[],[79,12])). % 1.05/1.15 cnf(111,plain, % 1.05/1.15 (P1(x1111,x1111)), % 1.05/1.15 inference(scs_inference,[],[40,7])). % 1.05/1.15 cnf(112,plain, % 1.05/1.15 (P1(x1121,x1122)+~P1(x1122,x1121)), % 1.05/1.15 inference(scs_inference,[],[111,14])). % 1.05/1.15 cnf(113,plain, % 1.05/1.15 (P1(x1131,x1131)), % 1.05/1.15 inference(rename_variables,[],[111])). % 1.05/1.15 cnf(114,plain, % 1.05/1.15 (~P1(x1141,f1(x1141,x1141))+~P1(f1(x1141,x1141),f1(x1141,x1141))), % 1.05/1.15 inference(scs_inference,[],[111,113,14,25])). % 1.05/1.15 cnf(118,plain, % 1.05/1.15 (P1(x1181,f1(x1181,f1(x1181,x1181)))+~P1(f1(x1181,x1181),f1(x1181,x1181))), % 1.05/1.15 inference(scs_inference,[],[111,113,14,25,57,80])). % 1.05/1.15 cnf(120,plain, % 1.05/1.15 (~P1(f1(x1201,x1201),f1(x1201,x1201))+P1(x1201,f1(f1(x1201,x1201),x1201))), % 1.05/1.15 inference(scs_inference,[],[111,113,14,25,57,80,8])). % 1.05/1.15 cnf(122,plain, % 1.05/1.15 (~P1(f1(x1221,x1221),f1(x1221,x1221))+~P1(f1(x1221,x1221),x1221)), % 1.05/1.15 inference(scs_inference,[],[111,113,14,25,57,80,8,10])). % 1.05/1.15 cnf(128,plain, % 1.05/1.15 (~P1(x1281,f1(x1281,x1281))), % 1.05/1.15 inference(scs_inference,[],[111,114])). % 1.05/1.15 cnf(129,plain, % 1.05/1.15 (P1(x1291,x1291)), % 1.05/1.15 inference(rename_variables,[],[111])). % 1.05/1.15 cnf(131,plain, % 1.05/1.15 (P1(x1311,x1311)), % 1.05/1.15 inference(rename_variables,[],[111])). % 1.05/1.15 cnf(133,plain, % 1.05/1.15 (P1(x1331,x1331)), % 1.05/1.15 inference(rename_variables,[],[111])). % 1.05/1.15 cnf(134,plain, % 1.05/1.15 (~P1(f1(x1341,x1341),x1341)), % 1.05/1.15 inference(scs_inference,[],[111,129,131,133,114,118,120,122])). % 1.05/1.15 cnf(136,plain, % 1.05/1.15 (P1(f1(x1361,x1361),f1(x1361,f1(x1361,x1361)))), % 1.05/1.15 inference(scs_inference,[],[111,129,131,133,114,118,120,122,8])). % 1.05/1.15 cnf(145,plain, % 1.05/1.15 ($false), % 1.05/1.15 inference(scs_inference,[],[128,134,136,112,7]), % 1.05/1.15 ['proof']). % 1.05/1.15 % SZS output end Proof % 1.05/1.15 % Total time :0.530000s %------------------------------------------------------------------------------