%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN332+1 : TPTP v8.2.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/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 : Theorem 1.15s 1.22s % Output : CNFRefutation 1.15s % 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 v2.0.0. % 0.11/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n021.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Sun Jun 23 23:00:09 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.56 start to proof:theBenchmark % 1.15/1.21 %------------------------------------------- % 1.15/1.21 % File :CSE---1.7 % 1.15/1.21 % Problem :theBenchmark % 1.15/1.21 % Transform :cnf % 1.15/1.21 % Format :tptp:raw % 1.15/1.21 % Command :java -jar mcs_scs.jar %d %s % 1.15/1.21 % 1.15/1.21 % Result :Theorem 0.610000s % 1.15/1.21 % Output :CNFRefutation 0.610000s % 1.15/1.21 %------------------------------------------- % 1.15/1.21 %-------------------------------------------------------------------------- % 1.15/1.21 % File : SYN332+1 : TPTP v8.2.0. Released v2.0.0. % 1.15/1.21 % Domain : Syntactic % 1.15/1.21 % Problem : Church problem 46.14 (4) % 1.15/1.21 % Version : Especial. % 1.15/1.22 % English : % 1.15/1.22 % 1.15/1.22 % Refs : [Chu56] Church (1956), Introduction to Mathematical Logic I % 1.15/1.22 % Source : [Chu56] % 1.15/1.22 % Names : 46.14 (4) [Chu56] % 1.15/1.22 % 1.15/1.22 % Status : Theorem % 1.15/1.22 % Rating : 0.06 v8.2.0, 0.07 v8.1.0, 0.00 v7.5.0, 0.05 v7.4.0, 0.06 v7.3.0, 0.14 v7.2.0, 0.00 v6.4.0, 0.07 v6.3.0, 0.08 v6.2.0, 0.00 v6.1.0, 0.04 v6.0.0, 0.00 v5.5.0, 0.08 v5.4.0, 0.09 v5.3.0, 0.17 v5.2.0, 0.14 v5.0.0, 0.15 v4.1.0, 0.17 v4.0.1, 0.21 v4.0.0, 0.30 v3.7.0, 0.33 v3.5.0, 0.25 v3.4.0, 0.17 v3.3.0, 0.22 v3.2.0, 0.33 v2.7.0, 0.00 v2.5.0, 0.33 v2.4.0, 0.33 v2.2.1, 0.00 v2.1.0 % 1.15/1.22 % Syntax : Number of formulae : 1 ( 0 unt; 0 def) % 1.15/1.22 % Number of atoms : 13 ( 0 equ) % 1.15/1.22 % Maximal formula atoms : 13 ( 13 avg) % 1.15/1.22 % Number of connectives : 12 ( 0 ~; 0 |; 1 &) % 1.15/1.22 % ( 5 <=>; 5 =>; 0 <=; 1 <~>) % 1.15/1.22 % Maximal formula depth : 10 ( 10 avg) % 1.15/1.22 % Maximal term depth : 1 ( 1 avg) % 1.15/1.22 % Number of predicates : 1 ( 1 usr; 0 prp; 2-2 aty) % 1.15/1.22 % Number of functors : 0 ( 0 usr; 0 con; --- aty) % 1.15/1.22 % Number of variables : 3 ( 1 !; 2 ?) % 1.15/1.22 % SPC : FOF_THM_RFO_NEQ % 1.15/1.22 % 1.15/1.22 % Comments : % 1.15/1.22 %-------------------------------------------------------------------------- % 1.15/1.22 fof(church_46_14_4,conjecture, % 1.15/1.22 ? [X,Y] : % 1.15/1.22 ! [Z] : % 1.15/1.22 ( ( ( big_f(X,Y) % 1.15/1.22 & big_f(Y,X) ) % 1.15/1.22 <~> big_f(X,Z) ) % 1.15/1.22 => ( ( big_f(X,Z) % 1.15/1.22 <=> big_f(Z,X) ) % 1.15/1.22 => ( ( big_f(X,Z) % 1.15/1.22 <=> big_f(Y,Z) ) % 1.15/1.22 => ( ( ( big_f(Y,X) % 1.15/1.22 => big_f(X,Y) ) % 1.15/1.22 <=> big_f(Z,Z) ) % 1.15/1.22 => ( ( big_f(X,Y) % 1.15/1.22 <=> big_f(Y,X) ) % 1.15/1.22 <=> big_f(Z,Y) ) ) ) ) ) ). % 1.15/1.22 % 1.15/1.22 %-------------------------------------------------------------------------- % 1.15/1.22 %------------------------------------------- % 1.15/1.22 % Proof found % 1.15/1.22 % SZS status Theorem for theBenchmark % 1.15/1.22 % SZS output start Proof % 1.15/1.22 %ClaNum:14(EqnAxiom:0) % 1.15/1.22 %VarNum:89(SingletonVarNum:28) % 1.15/1.22 %MaxLitNum:3 % 1.15/1.22 %MaxfuncDepth:1 % 1.15/1.22 %SharedTerms:0 % 1.15/1.22 %goalClause: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 % 1.15/1.22 [1]P1(x11,x12)+P1(x12,f1(x12,x11)) % 1.15/1.22 [2]P1(x21,x22)+P1(x21,f1(x21,x22)) % 1.15/1.22 [5]P1(x51,x52)+P1(f1(x52,x51),f1(x52,x51)) % 1.15/1.22 [6]~P1(x61,x62)+P1(f1(x61,x62),f1(x61,x62)) % 1.15/1.22 [8]P1(x81,f1(x81,x82))+~P1(x82,f1(x81,x82)) % 1.15/1.22 [9]P1(x91,f1(x92,x91))+~P1(x92,f1(x92,x91)) % 1.15/1.22 [10]P1(x101,f1(x101,x102))+~P1(f1(x101,x102),x101) % 1.15/1.22 [11]P1(f1(x111,x112),x111)+~P1(x111,f1(x111,x112)) % 1.15/1.22 [3]~P1(x32,x31)+P1(x31,x32)+P1(f1(x31,x32),x32) % 1.15/1.22 [4]~P1(x42,x41)+P1(x41,x42)+P1(f1(x42,x41),x41) % 1.15/1.22 [7]P1(x72,x71)+P1(x71,x72)+~P1(f1(x72,x71),x71) % 1.15/1.22 [12]~P1(x122,x121)+~P1(x121,x122)+~P1(x122,f1(x122,x121)) % 1.15/1.22 [13]~P1(x132,x131)+~P1(x131,x132)+~P1(f1(x132,x131),x131) % 1.15/1.22 [14]~P1(x142,x141)+P1(x141,x142)+~P1(f1(x141,x142),f1(x141,x142)) % 1.15/1.22 %EqnAxiom % 1.15/1.22 % 1.15/1.22 %------------------------------------------- % 1.15/1.22 cnf(25,plain, % 1.15/1.22 (~P1(x251,x252)+~P1(f1(x252,x251),f1(x252,x251))+~P1(x252,f1(x252,x251))), % 1.15/1.22 inference(scs_inference,[],[14,12])). % 1.15/1.22 cnf(40,plain, % 1.15/1.22 (P1(x401,x402)+P1(f1(x402,x401),x402)), % 1.15/1.22 inference(scs_inference,[],[1,11])). % 1.15/1.22 cnf(52,plain, % 1.15/1.22 (~P1(x521,f1(x521,x522))+~P1(x522,x521)+P1(f1(x521,x522),f1(f1(x521,x522),f1(x521,x522)))), % 1.15/1.22 inference(scs_inference,[],[1,25])). % 1.15/1.22 cnf(56,plain, % 1.15/1.22 (~P1(x561,x562)+P1(f1(x562,x561),f1(f1(x562,x561),f1(x562,x561)))+P1(f1(x562,x561),f1(f1(x562,x561),x562))), % 1.15/1.22 inference(scs_inference,[],[1,52])). % 1.15/1.22 cnf(57,plain, % 1.15/1.22 (P1(f1(x571,x572),f1(f1(x571,x572),x571))+~P1(f1(x571,x572),f1(x571,x572))+~P1(x572,x571)), % 1.15/1.22 inference(scs_inference,[],[56,12])). % 1.15/1.22 cnf(79,plain, % 1.15/1.22 (~P1(x791,x792)+P1(f1(x792,x791),f1(f1(x792,x791),f1(x792,x791)))+P1(x792,f1(x792,f1(x792,x791)))), % 1.15/1.22 inference(scs_inference,[],[2,52])). % 1.15/1.22 cnf(80,plain, % 1.15/1.22 (P1(x801,f1(x801,f1(x801,x802)))+~P1(f1(x801,x802),f1(x801,x802))+~P1(x802,x801)), % 1.15/1.22 inference(scs_inference,[],[79,12])). % 1.15/1.22 cnf(111,plain, % 1.15/1.22 (P1(x1111,x1111)), % 1.15/1.22 inference(scs_inference,[],[40,7])). % 1.15/1.22 cnf(112,plain, % 1.15/1.22 (P1(x1121,x1122)+~P1(x1122,x1121)), % 1.15/1.22 inference(scs_inference,[],[111,14])). % 1.15/1.22 cnf(113,plain, % 1.15/1.22 (P1(x1131,x1131)), % 1.15/1.22 inference(rename_variables,[],[111])). % 1.15/1.22 cnf(114,plain, % 1.15/1.22 (~P1(x1141,f1(x1141,x1141))+~P1(f1(x1141,x1141),f1(x1141,x1141))), % 1.15/1.22 inference(scs_inference,[],[111,113,14,25])). % 1.15/1.22 cnf(118,plain, % 1.15/1.22 (P1(x1181,f1(x1181,f1(x1181,x1181)))+~P1(f1(x1181,x1181),f1(x1181,x1181))), % 1.15/1.22 inference(scs_inference,[],[111,113,14,25,57,80])). % 1.15/1.22 cnf(120,plain, % 1.15/1.22 (~P1(f1(x1201,x1201),f1(x1201,x1201))+P1(x1201,f1(f1(x1201,x1201),x1201))), % 1.15/1.22 inference(scs_inference,[],[111,113,14,25,57,80,9])). % 1.15/1.22 cnf(122,plain, % 1.15/1.22 (~P1(f1(x1221,x1221),f1(x1221,x1221))+~P1(f1(x1221,x1221),x1221)), % 1.15/1.22 inference(scs_inference,[],[111,113,14,25,57,80,9,10])). % 1.15/1.22 cnf(128,plain, % 1.15/1.22 (~P1(x1281,f1(x1281,x1281))), % 1.15/1.22 inference(scs_inference,[],[111,114])). % 1.15/1.22 cnf(129,plain, % 1.15/1.22 (P1(x1291,x1291)), % 1.15/1.22 inference(rename_variables,[],[111])). % 1.15/1.22 cnf(131,plain, % 1.15/1.22 (P1(x1311,x1311)), % 1.15/1.22 inference(rename_variables,[],[111])). % 1.15/1.22 cnf(133,plain, % 1.15/1.22 (P1(x1331,x1331)), % 1.15/1.22 inference(rename_variables,[],[111])). % 1.15/1.22 cnf(134,plain, % 1.15/1.22 (~P1(f1(x1341,x1341),x1341)), % 1.15/1.22 inference(scs_inference,[],[111,129,131,133,114,118,120,122])). % 1.15/1.22 cnf(136,plain, % 1.15/1.22 (P1(f1(x1361,x1361),f1(x1361,f1(x1361,x1361)))), % 1.15/1.22 inference(scs_inference,[],[111,129,131,133,114,118,120,122,9])). % 1.15/1.22 cnf(145,plain, % 1.15/1.22 ($false), % 1.15/1.22 inference(scs_inference,[],[128,134,136,112,7]), % 1.15/1.22 ['proof']). % 1.15/1.22 % SZS output end Proof % 1.15/1.22 % Total time :0.610000s %------------------------------------------------------------------------------