%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN328+1 : TPTP v8.2.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n018.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:11 EDT 2024 % Result : Theorem 1.15s 1.23s % Output : CNFRefutation 1.24s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : SYN328+1 : TPTP v8.2.0. Released v2.0.0. % 0.03/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n018.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Sun Jun 23 23:31:09 EDT 2024 % 0.13/0.34 % CPUTime : % 0.53/0.58 start to proof:theBenchmark % 1.15/1.23 %------------------------------------------- % 1.15/1.23 % File :CSE---1.7 % 1.15/1.23 % Problem :theBenchmark % 1.15/1.23 % Transform :cnf % 1.15/1.23 % Format :tptp:raw % 1.15/1.23 % Command :java -jar mcs_scs.jar %d %s % 1.15/1.23 % 1.15/1.23 % Result :Theorem 0.610000s % 1.15/1.23 % Output :CNFRefutation 0.610000s % 1.15/1.23 %------------------------------------------- % 1.15/1.23 %-------------------------------------------------------------------------- % 1.15/1.23 % File : SYN328+1 : TPTP v8.2.0. Released v2.0.0. % 1.15/1.23 % Domain : Syntactic % 1.15/1.23 % Problem : Church problem 46.12 (3) % 1.15/1.23 % Version : Especial. % 1.15/1.23 % English : % 1.15/1.23 % 1.15/1.23 % Refs : [Chu56] Church (1956), Introduction to Mathematical Logic I % 1.15/1.23 % Source : [Chu56] % 1.15/1.23 % Names : 46.12 (3) [Chu56] % 1.15/1.23 % 1.15/1.23 % Status : Theorem % 1.15/1.23 % Rating : 0.00 v5.5.0, 0.04 v5.3.0, 0.13 v5.2.0, 0.07 v5.0.0, 0.05 v4.1.0, 0.06 v4.0.1, 0.05 v4.0.0, 0.10 v3.7.0, 0.33 v3.5.0, 0.12 v3.4.0, 0.08 v3.3.0, 0.11 v3.2.0, 0.33 v3.1.0, 0.17 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.23 % Syntax : Number of formulae : 1 ( 0 unt; 0 def) % 1.15/1.23 % Number of atoms : 13 ( 0 equ) % 1.15/1.23 % Maximal formula atoms : 13 ( 13 avg) % 1.15/1.23 % Number of connectives : 12 ( 0 ~; 0 |; 2 &) % 1.15/1.23 % ( 3 <=>; 7 =>; 0 <=; 0 <~>) % 1.15/1.23 % Maximal formula depth : 10 ( 10 avg) % 1.15/1.23 % Maximal term depth : 1 ( 1 avg) % 1.15/1.23 % Number of predicates : 3 ( 3 usr; 0 prp; 1-1 aty) % 1.15/1.23 % Number of functors : 0 ( 0 usr; 0 con; --- aty) % 1.15/1.23 % Number of variables : 3 ( 2 !; 1 ?) % 1.15/1.23 % SPC : FOF_THM_RFO_NEQ % 1.15/1.23 % 1.15/1.23 % Comments : % 1.15/1.23 %-------------------------------------------------------------------------- % 1.15/1.23 fof(church_46_12_3,conjecture, % 1.15/1.23 ? [X] : % 1.15/1.23 ! [Y,Z] : % 1.15/1.23 ( ( ( big_f(Y) % 1.15/1.23 => big_g(Y) ) % 1.15/1.23 <=> big_f(X) ) % 1.15/1.23 => ( ( ( big_f(Y) % 1.15/1.23 => big_h(Y) ) % 1.15/1.23 <=> big_g(X) ) % 1.15/1.23 => ( ( ( ( big_f(Y) % 1.15/1.23 => big_g(Y) ) % 1.15/1.23 => big_h(Y) ) % 1.15/1.23 <=> big_h(X) ) % 1.15/1.23 => ( big_f(Z) % 1.15/1.23 & big_g(Z) % 1.15/1.23 & big_h(Z) ) ) ) ) ). % 1.15/1.23 % 1.15/1.23 %-------------------------------------------------------------------------- % 1.15/1.23 %------------------------------------------- % 1.15/1.23 % Proof found % 1.15/1.23 % SZS status Theorem for theBenchmark % 1.15/1.23 % SZS output start Proof % 1.15/1.23 %ClaNum:11(EqnAxiom:0) % 1.15/1.23 %VarNum:28(SingletonVarNum:11) % 1.15/1.23 %MaxLitNum:3 % 1.15/1.23 %MaxfuncDepth:1 % 1.15/1.23 %SharedTerms:0 % 1.15/1.23 %goalClause: 1 2 3 4 5 6 7 8 9 10 11 % 1.15/1.23 [1]P1(x11)+P1(f1(x11)) % 1.15/1.23 [2]P2(x21)+P1(f1(x21)) % 1.15/1.23 [3]P1(x31)+~P2(f1(x31)) % 1.15/1.23 [4]P2(x41)+~P3(f1(x41)) % 1.15/1.23 [5]P3(x51)+~P3(f1(x51)) % 1.15/1.23 [6]~P3(x61)+P1(f1(x61))+P3(f1(x61)) % 1.15/1.23 [7]P3(x71)+P2(f1(x71))+~P1(f1(x71)) % 1.15/1.23 [8]~P1(x81)+P2(f1(x81))+~P1(f1(x81)) % 1.15/1.23 [9]~P2(x91)+P3(f1(x91))+~P1(f1(x91)) % 1.15/1.23 [10]~P3(x101)+P3(f1(x101))+~P2(f1(x101)) % 1.15/1.23 [11]~P2(f3(x111))+~P3(f4(x111))+~P1(f2(x111)) % 1.15/1.23 %EqnAxiom % 1.15/1.23 % 1.15/1.23 %------------------------------------------- % 1.15/1.24 cnf(18,plain, % 1.15/1.24 (P2(x181)+P2(f1(f1(x181)))+~P1(f1(f1(x181)))), % 1.15/1.24 inference(scs_inference,[],[7,4])). % 1.15/1.24 cnf(27,plain, % 1.15/1.24 (P2(f1(f1(x271)))+P2(f1(x271))+P2(x271)), % 1.15/1.24 inference(scs_inference,[],[2,18])). % 1.15/1.24 cnf(43,plain, % 1.15/1.24 (P3(x431)+~P2(f1(f1(x431)))+P2(f1(x431))), % 1.15/1.24 inference(scs_inference,[],[3,7])). % 1.15/1.24 cnf(44,plain, % 1.15/1.24 (P2(x441)+P3(x441)+P2(f1(x441))), % 1.15/1.24 inference(scs_inference,[],[43,27])). % 1.15/1.24 cnf(50,plain, % 1.15/1.24 (~P1(x501)+~P2(f1(f1(x501)))+P2(f1(x501))), % 1.15/1.24 inference(scs_inference,[],[3,8])). % 1.15/1.24 cnf(51,plain, % 1.15/1.24 (P2(x511)+~P1(x511)+P2(f1(x511))), % 1.15/1.24 inference(scs_inference,[],[50,27])). % 1.15/1.24 cnf(52,plain, % 1.15/1.24 (~P1(f1(x521))+P2(f1(f1(x521)))+P1(x521)), % 1.15/1.24 inference(scs_inference,[],[51,3])). % 1.15/1.24 cnf(53,plain, % 1.15/1.24 (P2(f1(f1(x531)))+P1(x531)), % 1.15/1.24 inference(scs_inference,[],[52,1])). % 1.15/1.24 cnf(57,plain, % 1.15/1.24 (~P2(x571)+~P2(f1(f1(x571)))+P3(f1(x571))), % 1.15/1.24 inference(scs_inference,[],[3,9])). % 1.15/1.24 cnf(68,plain, % 1.15/1.24 (P2(x681)+~P3(f1(f1(x681)))), % 1.15/1.24 inference(scs_inference,[],[4,5])). % 1.15/1.24 cnf(112,plain, % 1.15/1.24 (P2(f1(f1(x1121)))+P3(x1121)+P2(f1(x1121))), % 1.15/1.24 inference(scs_inference,[],[5,44])). % 1.15/1.24 cnf(113,plain, % 1.24/1.24 (P2(f1(x1131))+P3(x1131)), % 1.24/1.24 inference(scs_inference,[],[112,43])). % 1.24/1.24 cnf(116,plain, % 1.24/1.24 (P3(x1161)+P2(f1(f1(x1161)))), % 1.24/1.24 inference(scs_inference,[],[5,113])). % 1.24/1.24 cnf(128,plain, % 1.24/1.24 (~P2(f1(f1(x1281)))+P3(x1281)+~P2(x1281)), % 1.24/1.24 inference(scs_inference,[],[5,57])). % 1.24/1.24 cnf(129,plain, % 1.24/1.24 (~P2(x1291)+P3(x1291)), % 1.24/1.24 inference(scs_inference,[],[128,116])). % 1.24/1.24 cnf(133,plain, % 1.24/1.24 (P3(f1(f1(x1331)))+P1(x1331)), % 1.24/1.24 inference(scs_inference,[],[129,53])). % 1.24/1.24 cnf(134,plain, % 1.24/1.24 (P3(f1(f1(x1341)))+~P1(f1(x1341))+P2(f1(x1341))), % 1.24/1.24 inference(scs_inference,[],[133,8])). % 1.24/1.24 cnf(135,plain, % 1.24/1.24 (~P1(f1(x1351))+P2(f1(x1351))), % 1.24/1.24 inference(scs_inference,[],[134,4])). % 1.24/1.24 cnf(136,plain, % 1.24/1.24 (P2(f1(x1361))+P1(x1361)), % 1.24/1.24 inference(scs_inference,[],[135,1])). % 1.24/1.24 cnf(145,plain, % 1.24/1.24 (P3(x1451)+~P3(f1(f1(x1451)))), % 1.24/1.24 inference(scs_inference,[],[129,68])). % 1.24/1.24 cnf(163,plain, % 1.24/1.24 (P3(f1(x1631))+~P1(f1(x1631))), % 1.24/1.24 inference(scs_inference,[],[129,135])). % 1.24/1.24 cnf(164,plain, % 1.24/1.24 (~P1(f1(x1641))+P2(x1641)), % 1.24/1.24 inference(scs_inference,[],[163,4])). % 1.24/1.24 cnf(174,plain, % 1.24/1.24 (P3(f1(x1741))+P1(x1741)), % 1.24/1.24 inference(scs_inference,[],[129,136])). % 1.24/1.24 cnf(175,plain, % 1.24/1.24 (P3(f1(f1(x1751)))+P2(f1(x1751))), % 1.24/1.24 inference(scs_inference,[],[174,135])). % 1.24/1.24 cnf(176,plain, % 1.24/1.24 (P2(f1(x1761))), % 1.24/1.24 inference(scs_inference,[],[175,4])). % 1.24/1.24 cnf(177,plain, % 1.24/1.24 (P1(x1771)), % 1.24/1.24 inference(scs_inference,[],[176,3])). % 1.24/1.24 cnf(181,plain, % 1.24/1.24 (P3(x1811)), % 1.24/1.24 inference(scs_inference,[],[176,3,129,145])). % 1.24/1.24 cnf(184,plain, % 1.24/1.24 (~P1(f2(x1841))+~P3(f4(x1841))), % 1.24/1.24 inference(scs_inference,[],[176,3,129,145,164,11])). % 1.24/1.24 cnf(190,plain, % 1.24/1.24 ($false), % 1.24/1.24 inference(scs_inference,[],[177,181,184]), % 1.24/1.24 ['proof']). % 1.24/1.24 % SZS output end Proof % 1.24/1.24 % Total time :0.610000s %------------------------------------------------------------------------------