%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : ITP001+1 : TPTP v8.2.0. Bugfixed v7.5.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n004.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 09:07:40 EDT 2024 % Result : Theorem 0.55s 0.65s % Output : CNFRefutation 0.55s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.13 % Problem : ITP001+1 : TPTP v8.2.0. Bugfixed v7.5.0. % 0.08/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n004.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Tue Jun 18 23:15:39 EDT 2024 % 0.12/0.34 % CPUTime : % 0.19/0.56 start to proof:theBenchmark % 0.55/0.63 %------------------------------------------- % 0.55/0.63 % File :CSE---1.7 % 0.55/0.63 % Problem :theBenchmark % 0.55/0.63 % Transform :cnf % 0.55/0.63 % Format :tptp:raw % 0.55/0.63 % Command :java -jar mcs_scs.jar %d %s % 0.55/0.63 % 0.55/0.63 % Result :Theorem 0.000000s % 0.55/0.63 % Output :CNFRefutation 0.000000s % 0.55/0.63 %------------------------------------------- % 0.55/0.64 %------------------------------------------------------------------------------ % 0.55/0.64 % File : ITP001+1 : TPTP v8.2.0. Bugfixed v7.5.0. % 0.55/0.64 % Domain : Interactive Theorem Proving % 0.55/0.64 % Problem : HOL4 syntactic export of thm_2Ebool_2ETRUTH.p, bushy mode % 0.55/0.64 % Version : [BG+19] axioms. % 0.55/0.64 % English : % 0.55/0.64 % 0.55/0.64 % Refs : [BG+19] Brown et al. (2019), GRUNGE: A Grand Unified ATP Chall % 0.55/0.64 % : [Gau19] Gauthier (2019), Email to Geoff Sutcliffe % 0.55/0.64 % Source : [BG+19] % 0.55/0.64 % Names : thm_2Ebool_2ETRUTH.p [Gau19] % 0.55/0.64 % : HL400001+1.p [TPAP] % 0.55/0.64 % 0.55/0.64 % Status : Theorem % 0.55/0.64 % Rating : 0.03 v7.5.0 % 0.55/0.64 % Syntax : Number of formulae : 24 ( 8 unt; 0 def) % 0.55/0.64 % Number of atoms : 47 ( 13 equ) % 0.55/0.64 % Maximal formula atoms : 3 ( 1 avg) % 0.55/0.64 % Number of connectives : 26 ( 3 ~; 3 |; 2 &) % 0.55/0.64 % ( 14 <=>; 4 =>; 0 <=; 0 <~>) % 0.55/0.64 % Maximal formula depth : 7 ( 4 avg) % 0.55/0.64 % Maximal term depth : 11 ( 2 avg) % 0.55/0.64 % Number of predicates : 2 ( 1 usr; 0 prp; 1-2 aty) % 0.55/0.64 % Number of functors : 23 ( 23 usr; 13 con; 0-2 aty) % 0.55/0.64 % Number of variables : 51 ( 50 !; 1 ?) % 0.55/0.64 % SPC : FOF_THM_RFO_SEQ % 0.55/0.64 % 0.55/0.64 % Comments : % 0.55/0.64 % Bugfixes : v7.5.0 - Bugfixes in axioms and export. % 0.55/0.64 %------------------------------------------------------------------------------ % 0.55/0.64 fof(reserved_2Eho_2Eeq__ext,axiom, % 0.55/0.64 ! [A_27a,A_27b,V0f_2E0,V1g_2E0] : % 0.55/0.64 ( ! [V2x_2E0] : s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V0f_2E0),s(A_27a,V2x_2E0))) = s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V1g_2E0),s(A_27a,V2x_2E0))) % 0.55/0.64 => s(tyop_2Emin_2Efun(A_27a,A_27b),V0f_2E0) = s(tyop_2Emin_2Efun(A_27a,A_27b),V1g_2E0) ) ). % 0.55/0.64 % 0.55/0.64 fof(reserved_2Eho_2Eboolext,axiom, % 0.55/0.64 ! [V0_2E0,V1_2E0] : % 0.55/0.64 ( ( p(s(tyop_2Emin_2Ebool,V0_2E0)) % 0.55/0.64 <=> p(s(tyop_2Emin_2Ebool,V1_2E0)) ) % 0.55/0.64 => s(tyop_2Emin_2Ebool,V0_2E0) = s(tyop_2Emin_2Ebool,V1_2E0) ) ). % 0.55/0.64 % 0.55/0.64 fof(reserved_2Eho_2Etruth,axiom, % 0.55/0.64 p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ). % 0.55/0.64 % 0.55/0.64 fof(reserved_2Eho_2Enotfalse,axiom, % 0.55/0.64 ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ). % 0.55/0.64 % 0.55/0.64 fof(reserved_2Eho_2Ebool__cases__ax,axiom, % 0.55/0.64 ! [V0t_2E0] : % 0.55/0.64 ( s(tyop_2Emin_2Ebool,V0t_2E0) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) % 0.55/0.64 | s(tyop_2Emin_2Ebool,V0t_2E0) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) ) ). % 0.55/0.64 % 0.55/0.64 fof(reserved_2Eho_2Ei__thm,axiom, % 0.55/0.64 ! [A_27a,V0x_2E0] : s(A_27a,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27a),combin_i_2E0),s(A_27a,V0x_2E0))) = s(A_27a,V0x_2E0) ). % 0.55/0.64 % 0.55/0.64 fof(reserved_2Eho_2Ek__thm,axiom, % 0.55/0.64 ! [A_27a,A_27b,V0x_2E0,V1y_2E0] : s(A_27a,app_2E2(s(tyop_2Emin_2Efun(A_27b,A_27a),app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,A_27a)),combin_k_2E0),s(A_27a,V0x_2E0))),s(A_27b,V1y_2E0))) = s(A_27a,V0x_2E0) ). % 0.55/0.64 % 0.55/0.64 fof(reserved_2Eho_2Es__thm,axiom, % 0.55/0.64 ! [A_27a,A_27b,A_27c,V0f_2E0,V1g_2E0,V2x_2E0] : s(A_27c,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27c),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,A_27b),tyop_2Emin_2Efun(A_27a,A_27c)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,A_27c)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,A_27b),tyop_2Emin_2Efun(A_27a,A_27c))),combin_s_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,A_27c)),V0f_2E0))),s(tyop_2Emin_2Efun(A_27a,A_27b),V1g_2E0))),s(A_27a,V2x_2E0))) = s(A_27c,app_2E2(s(tyop_2Emin_2Efun(A_27b,A_27c),app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,A_27c)),V0f_2E0),s(A_27a,V2x_2E0))),s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V1g_2E0),s(A_27a,V2x_2E0))))) ). % 0.55/0.64 % 0.55/0.64 fof(reserved_2Elogic_2E_2F_5C,axiom, % 0.55/0.64 ! [V0_2E0,V1_2E0] : % 0.55/0.64 ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_2F_5C_2E2(s(tyop_2Emin_2Ebool,V0_2E0),s(tyop_2Emin_2Ebool,V1_2E0)))) % 0.55/0.64 <=> ( p(s(tyop_2Emin_2Ebool,V0_2E0)) % 0.55/0.64 & p(s(tyop_2Emin_2Ebool,V1_2E0)) ) ) ). % 0.55/0.64 % 0.55/0.64 fof(reserved_2Elogic_2E_5C_2F,axiom, % 0.55/0.64 ! [V0_2E0,V1_2E0] : % 0.55/0.64 ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_5C_2F_2E2(s(tyop_2Emin_2Ebool,V0_2E0),s(tyop_2Emin_2Ebool,V1_2E0)))) % 0.55/0.64 <=> ( p(s(tyop_2Emin_2Ebool,V0_2E0)) % 0.55/0.64 | p(s(tyop_2Emin_2Ebool,V1_2E0)) ) ) ). % 0.55/0.64 % 0.55/0.64 fof(reserved_2Elogic_2E_7E,axiom, % 0.55/0.64 ! [V0_2E0] : % 0.55/0.64 ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_7E_2E1(s(tyop_2Emin_2Ebool,V0_2E0)))) % 0.55/0.64 <=> ~ p(s(tyop_2Emin_2Ebool,V0_2E0)) ) ). % 0.55/0.64 % 0.55/0.64 fof(reserved_2Elogic_2E_3D_3D_3E,axiom, % 0.55/0.64 ! [V0_2E0,V1_2E0] : % 0.55/0.64 ( p(s(tyop_2Emin_2Ebool,c_2Emin_2E_3D_3D_3E_2E2(s(tyop_2Emin_2Ebool,V0_2E0),s(tyop_2Emin_2Ebool,V1_2E0)))) % 0.55/0.64 <=> ( p(s(tyop_2Emin_2Ebool,V0_2E0)) % 0.55/0.64 => p(s(tyop_2Emin_2Ebool,V1_2E0)) ) ) ). % 0.55/0.64 % 0.55/0.64 fof(reserved_2Elogic_2E_3D,axiom, % 0.55/0.64 ! [A_27a,V0_2E0,V1_2E0] : % 0.55/0.64 ( p(s(tyop_2Emin_2Ebool,c_2Emin_2E_3D_2E2(s(A_27a,V0_2E0),s(A_27a,V1_2E0)))) % 0.55/0.64 <=> s(A_27a,V0_2E0) = s(A_27a,V1_2E0) ) ). % 0.55/0.64 % 0.55/0.64 fof(reserved_2Equant_2E_21,axiom, % 0.55/0.64 ! [A_27a,V0f_2E0] : % 0.55/0.64 ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_21_2E1(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0f_2E0)))) % 0.55/0.64 <=> ! [V1x_2E0] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0f_2E0),s(A_27a,V1x_2E0)))) ) ). % 0.55/0.64 % 0.55/0.64 fof(reserved_2Equant_2E_3F,axiom, % 0.55/0.64 ! [A_27a,V0f_2E0] : % 0.55/0.64 ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0f_2E0)))) % 0.55/0.64 <=> ? [V1x_2E0] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0f_2E0),s(A_27a,V1x_2E0)))) ) ). % 0.55/0.64 % 0.55/0.64 fof(arityeq2_2Ec_2Ebool_2E_2F_5C_2E2,axiom, % 0.55/0.64 ! [X0_2E0,X1_2E0] : % 0.55/0.64 ( ( p(s(tyop_2Emin_2Ebool,X0_2E0)) % 0.55/0.64 & p(s(tyop_2Emin_2Ebool,X1_2E0)) ) % 0.55/0.64 <=> p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool)),c_2Ebool_2E_2F_5C_2E0),s(tyop_2Emin_2Ebool,X0_2E0))),s(tyop_2Emin_2Ebool,X1_2E0)))) ) ). % 0.55/0.64 % 0.55/0.64 fof(arityeq2_2Ec_2Ebool_2E_5C_2F_2E2,axiom, % 0.55/0.64 ! [X0_2E0,X1_2E0] : % 0.55/0.64 ( ( p(s(tyop_2Emin_2Ebool,X0_2E0)) % 0.55/0.64 | p(s(tyop_2Emin_2Ebool,X1_2E0)) ) % 0.55/0.64 <=> p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool)),c_2Ebool_2E_5C_2F_2E0),s(tyop_2Emin_2Ebool,X0_2E0))),s(tyop_2Emin_2Ebool,X1_2E0)))) ) ). % 0.55/0.64 % 0.55/0.64 fof(arityeq1_2Ec_2Ebool_2E_7E_2E1,axiom, % 0.55/0.64 ! [X0_2E0] : % 0.55/0.64 ( ~ p(s(tyop_2Emin_2Ebool,X0_2E0)) % 0.55/0.64 <=> p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),c_2Ebool_2E_7E_2E0),s(tyop_2Emin_2Ebool,X0_2E0)))) ) ). % 0.55/0.64 % 0.55/0.64 fof(arityeq2_2Ec_2Emin_2E_3D_3D_3E_2E2,axiom, % 0.55/0.64 ! [X0_2E0,X1_2E0] : % 0.55/0.64 ( ( p(s(tyop_2Emin_2Ebool,X0_2E0)) % 0.55/0.64 => p(s(tyop_2Emin_2Ebool,X1_2E0)) ) % 0.55/0.64 <=> p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool)),c_2Emin_2E_3D_3D_3E_2E0),s(tyop_2Emin_2Ebool,X0_2E0))),s(tyop_2Emin_2Ebool,X1_2E0)))) ) ). % 0.55/0.64 % 0.55/0.64 fof(arityeq2_2Ec_2Emin_2E_3D_2E2_2Emono_2EA_27a,axiom, % 0.55/0.64 ! [A_27a,X0_2E0,X1_2E0] : % 0.55/0.64 ( s(A_27a,X0_2E0) = s(A_27a,X1_2E0) % 0.55/0.64 <=> p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool)),c_2Emin_2E_3D_2E0),s(A_27a,X0_2E0))),s(A_27a,X1_2E0)))) ) ). % 0.55/0.64 % 0.55/0.64 fof(arityeq1_2Ec_2Ebool_2E_21_2E1_2Emono_2EA_27a,axiom, % 0.55/0.64 ! [A_27a,X0_2E0] : s(tyop_2Emin_2Ebool,c_2Ebool_2E_21_2E1(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X0_2E0))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),c_2Ebool_2E_21_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X0_2E0))) ). % 0.55/0.64 % 0.55/0.64 fof(arityeq1_2Ec_2Ebool_2E_3F_2E1_2Emono_2EA_27a,axiom, % 0.55/0.64 ! [A_27a,X0_2E0] : s(tyop_2Emin_2Ebool,c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X0_2E0))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),c_2Ebool_2E_3F_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X0_2E0))) ). % 0.55/0.64 % 0.55/0.64 fof(thm_2Ebool_2ET__DEF,axiom, % 0.55/0.64 ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) % 0.55/0.64 <=> ! [V0x_2E0] : s(tyop_2Emin_2Ebool,V0x_2E0) = s(tyop_2Emin_2Ebool,V0x_2E0) ) ). % 0.55/0.64 % 0.55/0.64 fof(thm_2Ebool_2ETRUTH,conjecture, % 0.55/0.64 p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ). % 0.55/0.64 % 0.55/0.65 %------------------------------------------------------------------------------ % 0.55/0.65 %------------------------------------------- % 0.55/0.65 % Proof found % 0.55/0.65 % SZS status Theorem for theBenchmark % 0.55/0.65 % SZS output start Proof % 0.55/0.65 %ClaNum:72(EqnAxiom:29) % 0.55/0.65 %VarNum:233(SingletonVarNum:87) % 0.55/0.65 %MaxLitNum:3 % 0.55/0.65 %MaxfuncDepth:5 % 0.55/0.65 %SharedTerms:24 % 0.55/0.65 %goalClause: 37 % 0.55/0.65 %singleGoalClaCount:1 % 0.55/0.65 [31]P1(f5(a1,a2)) % 0.55/0.65 [37]~P1(f5(a1,a2)) % 0.55/0.65 [38]~P1(f5(a1,a4)) % 0.55/0.65 [32]E(f5(x321,f3(f5(f26(x321,x321),a6),f5(x321,x322))),f5(x321,x322)) % 0.55/0.65 [33]E(f5(a1,f3(f5(f26(f26(x331,a1),a1),a7),f5(f26(x331,a1),x332))),f5(a1,f8(f5(f26(x331,a1),x332)))) % 0.55/0.65 [34]E(f5(a1,f3(f5(f26(f26(x341,a1),a1),a9),f5(f26(x341,a1),x342))),f5(a1,f12(f5(f26(x341,a1),x342)))) % 0.55/0.65 [35]E(f5(x351,f3(f5(f26(x352,x351),f3(f5(f26(x351,f26(x352,x351)),a21),f5(x351,x353))),f5(x352,x354))),f5(x351,x353)) % 0.55/0.65 [36]E(f5(x361,f3(f5(f26(x362,x361),f3(f5(f26(f26(x362,x363),f26(x362,x361)),f3(f5(f26(f26(x362,f26(x363,x361)),f26(f26(x362,x363),f26(x362,x361))),a22),f5(f26(x362,f26(x363,x361)),x364))),f5(f26(x362,x363),x365))),f5(x362,x366))),f5(x361,f3(f5(f26(x363,x361),f3(f5(f26(x362,f26(x363,x361)),x364),f5(x362,x366))),f5(x363,f3(f5(f26(x362,x363),x365),f5(x362,x366)))))) % 0.55/0.65 [39]E(f5(a1,x391),f5(a1,a2))+E(f5(a1,x391),f5(a1,a4)) % 0.55/0.65 [42]P1(f5(a1,x421))+P1(f5(a1,f13(f5(a1,x421)))) % 0.55/0.65 [43]~P1(f5(a1,x431))+~P1(f5(a1,f13(f5(a1,x431)))) % 0.55/0.65 [52]P1(f5(a1,x521))+P1(f5(a1,f3(f5(f26(a1,a1),a16),f5(a1,x521)))) % 0.55/0.65 [56]~P1(f5(a1,x561))+~P1(f5(a1,f3(f5(f26(a1,a1),a16),f5(a1,x561)))) % 0.55/0.65 [44]P1(f5(a1,x441))+P1(f5(a1,f17(f5(a1,x441),f5(a1,x442)))) % 0.55/0.65 [45]~P1(f5(a1,x452))+P1(f5(a1,f14(f5(a1,x451),f5(a1,x452)))) % 0.55/0.65 [46]~P1(f5(a1,x461))+P1(f5(a1,f14(f5(a1,x461),f5(a1,x462)))) % 0.55/0.65 [47]~P1(f5(a1,x472))+P1(f5(a1,f17(f5(a1,x471),f5(a1,x472)))) % 0.55/0.65 [50]P1(f5(a1,x501))+~P1(f5(a1,f10(f5(a1,x502),f5(a1,x501)))) % 0.55/0.65 [51]P1(f5(a1,x511))+~P1(f5(a1,f10(f5(a1,x511),f5(a1,x512)))) % 0.55/0.65 [61]P1(f5(a1,x611))+P1(f5(a1,f3(f5(f26(a1,a1),f3(f5(f26(a1,f26(a1,a1)),a20),f5(a1,x611))),f5(a1,x612)))) % 0.55/0.65 [62]~P1(f5(a1,x622))+P1(f5(a1,f3(f5(f26(a1,a1),f3(f5(f26(a1,f26(a1,a1)),a15),f5(a1,x621))),f5(a1,x622)))) % 0.55/0.65 [63]~P1(f5(a1,x631))+P1(f5(a1,f3(f5(f26(a1,a1),f3(f5(f26(a1,f26(a1,a1)),a15),f5(a1,x631))),f5(a1,x632)))) % 0.55/0.65 [64]~P1(f5(a1,x642))+P1(f5(a1,f3(f5(f26(a1,a1),f3(f5(f26(a1,f26(a1,a1)),a20),f5(a1,x641))),f5(a1,x642)))) % 0.55/0.65 [67]P1(f5(a1,x671))+~P1(f5(a1,f3(f5(f26(a1,a1),f3(f5(f26(a1,f26(a1,a1)),a11),f5(a1,x672))),f5(a1,x671)))) % 0.55/0.65 [68]P1(f5(a1,x681))+~P1(f5(a1,f3(f5(f26(a1,a1),f3(f5(f26(a1,f26(a1,a1)),a11),f5(a1,x681))),f5(a1,x682)))) % 0.55/0.65 [59]P1(f5(a1,f3(f5(f26(x591,a1),x592),f5(x591,f23(x591,x592)))))+~P1(f5(a1,f12(f5(f26(x591,a1),x592)))) % 0.55/0.65 [60]~P1(f5(a1,f3(f5(f26(x601,a1),x602),f5(x601,f24(x601,x602)))))+P1(f5(a1,f8(f5(f26(x601,a1),x602)))) % 0.55/0.65 [48]~E(f5(x481,x482),f5(x481,x483))+P1(f5(a1,f18(f5(x481,x482),f5(x481,x483)))) % 0.55/0.65 [54]E(f5(x541,x542),f5(x541,x543))+~P1(f5(a1,f18(f5(x541,x542),f5(x541,x543)))) % 0.55/0.65 [66]~E(f5(x661,x662),f5(x661,x663))+P1(f5(a1,f3(f5(f26(x661,a1),f3(f5(f26(x661,f26(x661,a1)),a19),f5(x661,x662))),f5(x661,x663)))) % 0.55/0.65 [71]E(f5(x711,x712),f5(x711,x713))+~P1(f5(a1,f3(f5(f26(x711,a1),f3(f5(f26(x711,f26(x711,a1)),a19),f5(x711,x712))),f5(x711,x713)))) % 0.55/0.65 [57]P1(f5(a1,f3(f5(f26(x571,a1),x572),f5(x571,x573))))+~P1(f5(a1,f8(f5(f26(x571,a1),x572)))) % 0.55/0.65 [58]~P1(f5(a1,f3(f5(f26(x581,a1),x582),f5(x581,x583))))+P1(f5(a1,f12(f5(f26(x581,a1),x582)))) % 0.55/0.65 [72]E(f5(f26(x721,x722),x723),f5(f26(x721,x722),x724))+~E(f5(x722,f3(f5(f26(x721,x722),x723),f5(x721,f25(x721,x722,x723,x724)))),f5(x722,f3(f5(f26(x721,x722),x724),f5(x721,f25(x721,x722,x723,x724))))) % 0.55/0.65 [40]E(f5(a1,x401),f5(a1,x402))+P1(f5(a1,x401))+P1(f5(a1,x402)) % 0.55/0.65 [41]E(f5(a1,x411),f5(a1,x412))+~P1(f5(a1,x411))+~P1(f5(a1,x412)) % 0.55/0.65 [49]~P1(f5(a1,x491))+~P1(f5(a1,x492))+P1(f5(a1,f10(f5(a1,x491),f5(a1,x492)))) % 0.55/0.65 [53]P1(f5(a1,x531))+P1(f5(a1,x532))+~P1(f5(a1,f14(f5(a1,x532),f5(a1,x531)))) % 0.55/0.65 [55]P1(f5(a1,x551))+~P1(f5(a1,x552))+~P1(f5(a1,f17(f5(a1,x552),f5(a1,x551)))) % 0.55/0.65 [65]~P1(f5(a1,x651))+~P1(f5(a1,x652))+P1(f5(a1,f3(f5(f26(a1,a1),f3(f5(f26(a1,f26(a1,a1)),a11),f5(a1,x651))),f5(a1,x652)))) % 0.55/0.65 [69]P1(f5(a1,x691))+P1(f5(a1,x692))+~P1(f5(a1,f3(f5(f26(a1,a1),f3(f5(f26(a1,f26(a1,a1)),a15),f5(a1,x692))),f5(a1,x691)))) % 0.55/0.65 [70]P1(f5(a1,x701))+~P1(f5(a1,x702))+~P1(f5(a1,f3(f5(f26(a1,a1),f3(f5(f26(a1,f26(a1,a1)),a20),f5(a1,x702))),f5(a1,x701)))) % 0.55/0.65 %EqnAxiom % 0.55/0.65 [1]E(x11,x11) % 0.55/0.65 [2]E(x22,x21)+~E(x21,x22) % 0.55/0.65 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.55/0.65 [4]~E(x41,x42)+E(f5(x41,x43),f5(x42,x43)) % 0.55/0.65 [5]~E(x51,x52)+E(f5(x53,x51),f5(x53,x52)) % 0.55/0.65 [6]~E(x61,x62)+E(f3(x61,x63),f3(x62,x63)) % 0.55/0.65 [7]~E(x71,x72)+E(f3(x73,x71),f3(x73,x72)) % 0.55/0.65 [8]~E(x81,x82)+E(f26(x81,x83),f26(x82,x83)) % 0.55/0.65 [9]~E(x91,x92)+E(f26(x93,x91),f26(x93,x92)) % 0.55/0.65 [10]~E(x101,x102)+E(f25(x101,x103,x104,x105),f25(x102,x103,x104,x105)) % 0.55/0.65 [11]~E(x111,x112)+E(f25(x113,x111,x114,x115),f25(x113,x112,x114,x115)) % 0.55/0.65 [12]~E(x121,x122)+E(f25(x123,x124,x121,x125),f25(x123,x124,x122,x125)) % 0.55/0.65 [13]~E(x131,x132)+E(f25(x133,x134,x135,x131),f25(x133,x134,x135,x132)) % 0.55/0.65 [14]~E(x141,x142)+E(f13(x141),f13(x142)) % 0.55/0.65 [15]~E(x151,x152)+E(f10(x151,x153),f10(x152,x153)) % 0.55/0.65 [16]~E(x161,x162)+E(f10(x163,x161),f10(x163,x162)) % 0.55/0.65 [17]~E(x171,x172)+E(f17(x171,x173),f17(x172,x173)) % 0.55/0.65 [18]~E(x181,x182)+E(f17(x183,x181),f17(x183,x182)) % 0.55/0.65 [19]~E(x191,x192)+E(f12(x191),f12(x192)) % 0.55/0.65 [20]~E(x201,x202)+E(f23(x201,x203),f23(x202,x203)) % 0.55/0.65 [21]~E(x211,x212)+E(f23(x213,x211),f23(x213,x212)) % 0.55/0.65 [22]~E(x221,x222)+E(f14(x221,x223),f14(x222,x223)) % 0.55/0.65 [23]~E(x231,x232)+E(f14(x233,x231),f14(x233,x232)) % 0.55/0.65 [24]~E(x241,x242)+E(f24(x241,x243),f24(x242,x243)) % 0.55/0.65 [25]~E(x251,x252)+E(f24(x253,x251),f24(x253,x252)) % 0.55/0.65 [26]~E(x261,x262)+E(f8(x261),f8(x262)) % 0.55/0.65 [27]~E(x271,x272)+E(f18(x271,x273),f18(x272,x273)) % 0.55/0.65 [28]~E(x281,x282)+E(f18(x283,x281),f18(x283,x282)) % 0.55/0.65 [29]~P1(x291)+P1(x292)+~E(x291,x292) % 0.55/0.65 % 0.55/0.65 %------------------------------------------- % 0.55/0.65 cnf(76,plain, % 0.55/0.65 ($false), % 0.55/0.65 inference(scs_inference,[],[37,31]), % 0.55/0.65 ['proof']). % 0.55/0.65 % SZS output end Proof % 0.55/0.65 % Total time :0.000000s %------------------------------------------------------------------------------