%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : ALG216+1 : TPTP v8.2.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n019.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 03:41:01 EDT 2024 % Result : Theorem 47.47s 47.54s % Output : CNFRefutation 47.47s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.02/0.10 % Problem : ALG216+1 : TPTP v8.2.0. Released v3.4.0. % 0.02/0.10 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.10/0.31 % Computer : n019.cluster.edu % 0.10/0.31 % Model : x86_64 x86_64 % 0.10/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.31 % Memory : 8042.1875MB % 0.10/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.31 % CPULimit : 300 % 0.10/0.31 % WCLimit : 300 % 0.10/0.31 % DateTime : Wed Jun 19 17:44:09 EDT 2024 % 0.10/0.31 % CPUTime : % 0.16/0.55 start to proof:theBenchmark % 47.43/47.52 %------------------------------------------- % 47.43/47.52 % File :CSE---1.7 % 47.43/47.52 % Problem :theBenchmark % 47.43/47.52 % Transform :cnf % 47.43/47.52 % Format :tptp:raw % 47.43/47.52 % Command :java -jar mcs_scs.jar %d %s % 47.43/47.52 % 47.43/47.52 % Result :Theorem 46.910000s % 47.43/47.52 % Output :CNFRefutation 46.910000s % 47.43/47.52 %------------------------------------------- % 47.47/47.53 %------------------------------------------------------------------------------ % 47.47/47.53 % File : ALG216+1 : TPTP v8.2.0. Released v3.4.0. % 47.47/47.53 % Domain : General Algebra % 47.47/47.53 % Problem : Linear Independence in Right Module over Domain T06 % 47.47/47.53 % Version : [Urb08] axioms : Especial. % 47.47/47.53 % English : % 47.47/47.53 % 47.47/47.53 % Refs : [Urb07] Urban (2007), MPTP 0.2: Design, Implementation, and In % 47.47/47.53 % : [Urb08] Urban (2006), Email to G. Sutcliffe % 47.47/47.53 % Source : [Urb08] % 47.47/47.53 % Names : t6_rmod_5 [Urb08] % 47.47/47.53 % 47.47/47.53 % Status : Theorem % 47.47/47.53 % Rating : 0.31 v8.2.0, 0.25 v8.1.0, 0.28 v7.4.0, 0.13 v7.3.0, 0.24 v7.2.0, 0.21 v7.1.0, 0.22 v7.0.0, 0.17 v6.4.0, 0.23 v6.3.0, 0.25 v6.2.0, 0.32 v6.1.0, 0.40 v6.0.0, 0.35 v5.5.0, 0.56 v5.4.0, 0.57 v5.3.0, 0.59 v5.2.0, 0.50 v5.1.0, 0.48 v5.0.0, 0.50 v4.1.0, 0.57 v4.0.0, 0.58 v3.7.0, 0.55 v3.5.0, 0.58 v3.4.0 % 47.47/47.53 % Syntax : Number of formulae : 53 ( 21 unt; 0 def) % 47.47/47.53 % Number of atoms : 151 ( 9 equ) % 47.47/47.53 % Maximal formula atoms : 23 ( 2 avg) % 47.47/47.53 % Number of connectives : 130 ( 32 ~; 2 |; 62 &) % 47.47/47.53 % ( 1 <=>; 33 =>; 0 <=; 0 <~>) % 47.47/47.53 % Maximal formula depth : 13 ( 4 avg) % 47.47/47.53 % Maximal term depth : 3 ( 1 avg) % 47.47/47.53 % Number of predicates : 26 ( 24 usr; 1 prp; 0-3 aty) % 47.47/47.53 % Number of functors : 7 ( 7 usr; 1 con; 0-3 aty) % 47.47/47.53 % Number of variables : 78 ( 60 !; 18 ?) % 47.47/47.53 % SPC : FOF_THM_RFO_SEQ % 47.47/47.53 % 47.47/47.53 % Comments : Normal version: includes the axioms (which may be theorems from % 47.47/47.53 % other articles) and background that are possibly necessary. % 47.47/47.53 % : Translated by MPTP from the Mizar Mathematical Library 4.48.930. % 47.47/47.53 % : The problem encoding is based on set theory. % 47.47/47.53 %------------------------------------------------------------------------------ % 47.47/47.53 fof(t6_rmod_5,conjecture, % 47.47/47.53 ! [A] : % 47.47/47.53 ( ( ~ v3_struct_0(A) % 47.47/47.53 & v3_rlvect_1(A) % 47.47/47.53 & v4_rlvect_1(A) % 47.47/47.53 & v5_rlvect_1(A) % 47.47/47.53 & v6_rlvect_1(A) % 47.47/47.53 & v4_group_1(A) % 47.47/47.53 & v6_vectsp_1(A) % 47.47/47.53 & v7_vectsp_1(A) % 47.47/47.53 & v8_vectsp_1(A) % 47.47/47.53 & l3_vectsp_1(A) ) % 47.47/47.53 => ! [B] : % 47.47/47.53 ( ( ~ v3_struct_0(B) % 47.47/47.53 & v3_rlvect_1(B) % 47.47/47.53 & v4_rlvect_1(B) % 47.47/47.53 & v5_rlvect_1(B) % 47.47/47.53 & v6_rlvect_1(B) % 47.47/47.53 & v5_vectsp_2(B,A) % 47.47/47.53 & l1_vectsp_2(B,A) ) % 47.47/47.53 => ! [C] : % 47.47/47.53 ( m1_subset_1(C,u1_struct_0(B)) % 47.47/47.53 => ( k1_rlvect_1(A) != k2_group_1(A) % 47.47/47.53 => ( ~ v1_rmod_5(k8_rlvect_2(B,C,k1_rlvect_1(B)),A,B) % 47.47/47.53 & ~ v1_rmod_5(k8_rlvect_2(B,k1_rlvect_1(B),C),A,B) ) ) ) ) ) ). % 47.47/47.53 % 47.47/47.53 fof(antisymmetry_r2_hidden,axiom, % 47.47/47.53 ! [A,B] : % 47.47/47.53 ( r2_hidden(A,B) % 47.47/47.53 => ~ r2_hidden(B,A) ) ). % 47.47/47.53 % 47.47/47.53 fof(dt_k1_xboole_0,axiom, % 47.47/47.53 $true ). % 47.47/47.53 % 47.47/47.53 fof(fc1_xboole_0,axiom, % 47.47/47.53 v1_xboole_0(k1_xboole_0) ). % 47.47/47.53 % 47.47/47.53 fof(t1_subset,axiom, % 47.47/47.53 ! [A,B] : % 47.47/47.53 ( r2_hidden(A,B) % 47.47/47.53 => m1_subset_1(A,B) ) ). % 47.47/47.53 % 47.47/47.53 fof(t4_subset,axiom, % 47.47/47.53 ! [A,B,C] : % 47.47/47.53 ( ( r2_hidden(A,B) % 47.47/47.53 & m1_subset_1(B,k1_zfmisc_1(C)) ) % 47.47/47.53 => m1_subset_1(A,C) ) ). % 47.47/47.53 % 47.47/47.53 fof(t5_subset,axiom, % 47.47/47.53 ! [A,B,C] : % 47.47/47.53 ~ ( r2_hidden(A,B) % 47.47/47.53 & m1_subset_1(B,k1_zfmisc_1(C)) % 47.47/47.53 & v1_xboole_0(C) ) ). % 47.47/47.53 % 47.47/47.53 fof(reflexivity_r1_tarski,axiom, % 47.47/47.53 ! [A,B] : r1_tarski(A,A) ). % 47.47/47.53 % 47.47/47.53 fof(existence_l1_vectsp_1,axiom, % 47.47/47.53 ? [A] : l1_vectsp_1(A) ). % 47.47/47.53 % 47.47/47.53 fof(dt_l1_vectsp_1,axiom, % 47.47/47.53 ! [A] : % 47.47/47.53 ( l1_vectsp_1(A) % 47.47/47.53 => l1_group_1(A) ) ). % 47.47/47.53 % 47.47/47.53 fof(rc1_subset_1,axiom, % 47.47/47.53 ! [A] : % 47.47/47.53 ( ~ v1_xboole_0(A) % 47.47/47.53 => ? [B] : % 47.47/47.54 ( m1_subset_1(B,k1_zfmisc_1(A)) % 47.47/47.54 & ~ v1_xboole_0(B) ) ) ). % 47.47/47.54 % 47.47/47.54 fof(rc1_xboole_0,axiom, % 47.47/47.54 ? [A] : v1_xboole_0(A) ). % 47.47/47.54 % 47.47/47.54 fof(rc2_rlvect_2,axiom, % 47.47/47.54 ! [A] : % 47.47/47.54 ( ( ~ v3_struct_0(A) % 47.47/47.54 & l1_struct_0(A) ) % 47.47/47.54 => ? [B] : % 47.47/47.54 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 47.47/47.54 & ~ v1_xboole_0(B) % 47.47/47.54 & v1_finset_1(B) ) ) ). % 47.47/47.54 % 47.47/47.54 fof(rc2_subset_1,axiom, % 47.47/47.54 ! [A] : % 47.47/47.54 ? [B] : % 47.47/47.54 ( m1_subset_1(B,k1_zfmisc_1(A)) % 47.47/47.54 & v1_xboole_0(B) ) ). % 47.47/47.54 % 47.47/47.54 fof(rc2_xboole_0,axiom, % 47.47/47.54 ? [A] : ~ v1_xboole_0(A) ). % 47.47/47.54 % 47.47/47.54 fof(rc5_struct_0,axiom, % 47.47/47.54 ! [A] : % 47.47/47.54 ( ( ~ v3_struct_0(A) % 47.47/47.54 & l1_struct_0(A) ) % 47.47/47.54 => ? [B] : % 47.47/47.54 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 47.47/47.54 & ~ v1_xboole_0(B) ) ) ). % 47.47/47.54 % 47.47/47.54 fof(t2_subset,axiom, % 47.47/47.54 ! [A,B] : % 47.47/47.54 ( m1_subset_1(A,B) % 47.47/47.54 => ( v1_xboole_0(B) % 47.47/47.54 | r2_hidden(A,B) ) ) ). % 47.47/47.54 % 47.47/47.54 fof(t6_boole,axiom, % 47.47/47.54 ! [A] : % 47.47/47.54 ( v1_xboole_0(A) % 47.47/47.54 => A = k1_xboole_0 ) ). % 47.47/47.54 % 47.47/47.54 fof(t7_boole,axiom, % 47.47/47.54 ! [A,B] : % 47.47/47.54 ~ ( r2_hidden(A,B) % 47.47/47.54 & v1_xboole_0(B) ) ). % 47.47/47.54 % 47.47/47.54 fof(t8_boole,axiom, % 47.47/47.54 ! [A,B] : % 47.47/47.54 ~ ( v1_xboole_0(A) % 47.47/47.54 & A != B % 47.47/47.54 & v1_xboole_0(B) ) ). % 47.47/47.54 % 47.47/47.54 fof(commutativity_k2_tarski,axiom, % 47.47/47.54 ! [A,B] : k2_tarski(A,B) = k2_tarski(B,A) ). % 47.47/47.54 % 47.47/47.54 fof(existence_l1_group_1,axiom, % 47.47/47.54 ? [A] : l1_group_1(A) ). % 47.47/47.54 % 47.47/47.54 fof(existence_l1_rlvect_1,axiom, % 47.47/47.54 ? [A] : l1_rlvect_1(A) ). % 47.47/47.54 % 47.47/47.54 fof(existence_l1_struct_0,axiom, % 47.47/47.54 ? [A] : l1_struct_0(A) ). % 47.47/47.54 % 47.47/47.54 fof(existence_l2_struct_0,axiom, % 47.47/47.54 ? [A] : l2_struct_0(A) ). % 47.47/47.54 % 47.47/47.54 fof(existence_l2_vectsp_1,axiom, % 47.47/47.54 ? [A] : l2_vectsp_1(A) ). % 47.47/47.54 % 47.47/47.54 fof(dt_k1_zfmisc_1,axiom, % 47.47/47.54 $true ). % 47.47/47.54 % 47.47/47.54 fof(dt_k2_tarski,axiom, % 47.47/47.54 $true ). % 47.47/47.54 % 47.47/47.54 fof(dt_l1_group_1,axiom, % 47.47/47.54 ! [A] : % 47.47/47.54 ( l1_group_1(A) % 47.47/47.54 => l1_struct_0(A) ) ). % 47.47/47.54 % 47.47/47.54 fof(dt_l1_rlvect_1,axiom, % 47.47/47.54 ! [A] : % 47.47/47.54 ( l1_rlvect_1(A) % 47.47/47.54 => l2_struct_0(A) ) ). % 47.47/47.54 % 47.47/47.54 fof(dt_l1_struct_0,axiom, % 47.47/47.54 $true ). % 47.47/47.54 % 47.47/47.54 fof(dt_l2_struct_0,axiom, % 47.47/47.54 ! [A] : % 47.47/47.54 ( l2_struct_0(A) % 47.47/47.54 => l1_struct_0(A) ) ). % 47.47/47.54 % 47.47/47.54 fof(dt_l2_vectsp_1,axiom, % 47.47/47.54 ! [A] : % 47.47/47.54 ( l2_vectsp_1(A) % 47.47/47.54 => ( l1_vectsp_1(A) % 47.47/47.54 & l2_struct_0(A) ) ) ). % 47.47/47.54 % 47.47/47.54 fof(fc1_struct_0,axiom, % 47.47/47.54 ! [A] : % 47.47/47.54 ( ( ~ v3_struct_0(A) % 47.47/47.54 & l1_struct_0(A) ) % 47.47/47.54 => ~ v1_xboole_0(u1_struct_0(A)) ) ). % 47.47/47.54 % 47.47/47.54 fof(fc1_subset_1,axiom, % 47.47/47.54 ! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)) ). % 47.47/47.54 % 47.47/47.54 fof(fc3_subset_1,axiom, % 47.47/47.54 ! [A,B] : ~ v1_xboole_0(k2_tarski(A,B)) ). % 47.47/47.54 % 47.47/47.54 fof(rc3_struct_0,axiom, % 47.47/47.54 ? [A] : % 47.47/47.54 ( l1_struct_0(A) % 47.47/47.54 & ~ v3_struct_0(A) ) ). % 47.47/47.54 % 47.47/47.54 fof(rc4_struct_0,axiom, % 47.47/47.54 ? [A] : % 47.47/47.54 ( l2_struct_0(A) % 47.47/47.54 & ~ v3_struct_0(A) ) ). % 47.47/47.54 % 47.47/47.54 fof(rc9_vectsp_2,axiom, % 47.47/47.54 ! [A] : % 47.47/47.54 ( l1_struct_0(A) % 47.47/47.54 => ? [B] : % 47.47/47.54 ( l1_vectsp_2(B,A) % 47.47/47.54 & ~ v3_struct_0(B) ) ) ). % 47.47/47.54 % 47.47/47.54 fof(t3_subset,axiom, % 47.47/47.54 ! [A,B] : % 47.47/47.54 ( m1_subset_1(A,k1_zfmisc_1(B)) % 47.47/47.54 <=> r1_tarski(A,B) ) ). % 47.47/47.54 % 47.47/47.54 fof(commutativity_k8_rlvect_2,axiom, % 47.47/47.54 ! [A,B,C] : % 47.47/47.54 ( ( ~ v3_struct_0(A) % 47.47/47.54 & l1_struct_0(A) % 47.47/47.54 & m1_subset_1(B,u1_struct_0(A)) % 47.47/47.54 & m1_subset_1(C,u1_struct_0(A)) ) % 47.47/47.54 => k8_rlvect_2(A,B,C) = k8_rlvect_2(A,C,B) ) ). % 47.47/47.54 % 47.47/47.54 fof(existence_l1_vectsp_2,axiom, % 47.47/47.54 ! [A] : % 47.47/47.54 ( l1_struct_0(A) % 47.47/47.54 => ? [B] : l1_vectsp_2(B,A) ) ). % 47.47/47.54 % 47.47/47.54 fof(existence_l3_vectsp_1,axiom, % 47.47/47.54 ? [A] : l3_vectsp_1(A) ). % 47.47/47.54 % 47.47/47.54 fof(existence_m1_subset_1,axiom, % 47.47/47.54 ! [A] : % 47.47/47.54 ? [B] : m1_subset_1(B,A) ). % 47.47/47.54 % 47.47/47.54 fof(redefinition_k8_rlvect_2,axiom, % 47.47/47.54 ! [A,B,C] : % 47.47/47.54 ( ( ~ v3_struct_0(A) % 47.47/47.54 & l1_struct_0(A) % 47.47/47.54 & m1_subset_1(B,u1_struct_0(A)) % 47.47/47.54 & m1_subset_1(C,u1_struct_0(A)) ) % 47.47/47.54 => k8_rlvect_2(A,B,C) = k2_tarski(B,C) ) ). % 47.47/47.54 % 47.47/47.54 fof(dt_k1_rlvect_1,axiom, % 47.47/47.54 ! [A] : % 47.47/47.54 ( l2_struct_0(A) % 47.47/47.54 => m1_subset_1(k1_rlvect_1(A),u1_struct_0(A)) ) ). % 47.47/47.54 % 47.47/47.54 fof(dt_k2_group_1,axiom, % 47.47/47.54 ! [A] : % 47.47/47.54 ( ( ~ v3_struct_0(A) % 47.47/47.54 & l1_group_1(A) ) % 47.47/47.54 => m1_subset_1(k2_group_1(A),u1_struct_0(A)) ) ). % 47.47/47.54 % 47.47/47.54 fof(dt_k8_rlvect_2,axiom, % 47.47/47.54 ! [A,B,C] : % 47.47/47.54 ( ( ~ v3_struct_0(A) % 47.47/47.54 & l1_struct_0(A) % 47.47/47.54 & m1_subset_1(B,u1_struct_0(A)) % 47.47/47.54 & m1_subset_1(C,u1_struct_0(A)) ) % 47.47/47.54 => ( v1_finset_1(k8_rlvect_2(A,B,C)) % 47.47/47.54 & m1_subset_1(k8_rlvect_2(A,B,C),k1_zfmisc_1(u1_struct_0(A))) ) ) ). % 47.47/47.54 % 47.47/47.54 fof(dt_l1_vectsp_2,axiom, % 47.47/47.54 ! [A] : % 47.47/47.54 ( l1_struct_0(A) % 47.47/47.54 => ! [B] : % 47.47/47.54 ( l1_vectsp_2(B,A) % 47.47/47.54 => l1_rlvect_1(B) ) ) ). % 47.47/47.54 % 47.47/47.54 fof(dt_l3_vectsp_1,axiom, % 47.47/47.54 ! [A] : % 47.47/47.54 ( l3_vectsp_1(A) % 47.47/47.54 => ( l1_rlvect_1(A) % 47.47/47.54 & l2_vectsp_1(A) ) ) ). % 47.47/47.54 % 47.47/47.54 fof(dt_m1_subset_1,axiom, % 47.47/47.54 $true ). % 47.47/47.54 % 47.47/47.54 fof(dt_u1_struct_0,axiom, % 47.47/47.54 $true ). % 47.47/47.54 % 47.47/47.54 fof(t5_rmod_5,axiom, % 47.47/47.54 ! [A] : % 47.47/47.54 ( ( ~ v3_struct_0(A) % 47.47/47.54 & v3_rlvect_1(A) % 47.47/47.54 & v4_rlvect_1(A) % 47.47/47.54 & v5_rlvect_1(A) % 47.47/47.54 & v6_rlvect_1(A) % 47.47/47.54 & v4_group_1(A) % 47.47/47.54 & v6_vectsp_1(A) % 47.47/47.54 & v7_vectsp_1(A) % 47.47/47.54 & v8_vectsp_1(A) % 47.47/47.54 & l3_vectsp_1(A) ) % 47.47/47.54 => ! [B] : % 47.47/47.54 ( ( ~ v3_struct_0(B) % 47.47/47.54 & v3_rlvect_1(B) % 47.47/47.54 & v4_rlvect_1(B) % 47.47/47.54 & v5_rlvect_1(B) % 47.47/47.54 & v6_rlvect_1(B) % 47.47/47.54 & v5_vectsp_2(B,A) % 47.47/47.54 & l1_vectsp_2(B,A) ) % 47.47/47.54 => ! [C] : % 47.47/47.54 ( m1_subset_1(C,u1_struct_0(B)) % 47.47/47.54 => ! [D] : % 47.47/47.54 ( m1_subset_1(D,u1_struct_0(B)) % 47.47/47.54 => ( v1_rmod_5(k8_rlvect_2(B,C,D),A,B) % 47.47/47.54 => ( k1_rlvect_1(A) = k2_group_1(A) % 47.47/47.54 | ( C != k1_rlvect_1(B) % 47.47/47.54 & D != k1_rlvect_1(B) ) ) ) ) ) ) ) ). % 47.47/47.54 % 47.47/47.54 %------------------------------------------------------------------------------ % 47.47/47.54 %------------------------------------------- % 47.47/47.54 % Proof found % 47.47/47.54 % SZS status Theorem for theBenchmark % 47.47/47.54 % SZS output start Proof % 47.47/47.54 %ClaNum:129(EqnAxiom:50) % 47.47/47.54 %VarNum:221(SingletonVarNum:73) % 47.47/47.54 %MaxLitNum:22 % 47.47/47.54 %MaxfuncDepth:2 % 47.47/47.54 %SharedTerms:56 % 47.47/47.54 %goalClause: 51 52 53 54 55 56 57 58 59 60 61 62 63 76 77 79 83 84 88 127 % 47.47/47.54 %singleGoalClaCount:19 % 47.47/47.54 [51]P1(a1) % 47.47/47.54 [52]P1(a12) % 47.47/47.54 [53]P16(a1) % 47.47/47.54 [54]P16(a12) % 47.47/47.54 [55]P19(a1) % 47.47/47.54 [56]P19(a12) % 47.47/47.54 [57]P20(a1) % 47.47/47.54 [58]P20(a12) % 47.47/47.54 [59]P17(a1) % 47.47/47.54 [60]P22(a1) % 47.47/47.54 [61]P23(a1) % 47.47/47.54 [62]P24(a1) % 47.47/47.54 [63]P2(a1) % 47.47/47.54 [64]P2(a13) % 47.47/47.54 [65]P10(a15) % 47.47/47.54 [66]P10(a16) % 47.47/47.54 [67]P3(a17) % 47.47/47.54 [68]P4(a2) % 47.47/47.54 [69]P5(a4) % 47.47/47.54 [70]P5(a6) % 47.47/47.54 [71]P6(a5) % 47.47/47.54 [72]P7(a7) % 47.47/47.54 [73]P7(a9) % 47.47/47.54 [74]P9(a8) % 47.47/47.54 [76]P21(a12,a1) % 47.47/47.54 [77]P8(a12,a1) % 47.47/47.54 [83]~P18(a1) % 47.47/47.54 [84]~P18(a12) % 47.47/47.54 [85]~P18(a6) % 47.47/47.54 [86]~P18(a9) % 47.47/47.54 [87]~P10(a22) % 47.47/47.54 [79]P12(a18,f24(a12)) % 47.47/47.54 [88]~E(f27(a1),f23(a1)) % 47.47/47.54 [78]P11(x781,x781) % 47.47/47.54 [75]P10(f20(x751)) % 47.47/47.54 [80]P12(f14(x801),x801) % 47.47/47.54 [81]P12(f20(x811),f25(x811)) % 47.47/47.54 [89]~P10(f25(x891)) % 47.47/47.54 [82]E(f26(x821,x822),f26(x822,x821)) % 47.47/47.54 [90]~P10(f26(x901,x902)) % 47.47/47.54 [127]P15(f28(a12,a18,f23(a12)),a1,a12)+P15(f28(a12,f23(a12),a18),a1,a12) % 47.47/47.54 [91]~P10(x911)+E(x911,a15) % 47.47/47.54 [92]~P9(x921)+P3(x921) % 47.47/47.54 [93]~P3(x931)+P4(x931) % 47.47/47.54 [94]~P4(x941)+P5(x941) % 47.47/47.54 [95]~P7(x951)+P5(x951) % 47.47/47.54 [96]~P2(x961)+P6(x961) % 47.47/47.54 [97]~P6(x971)+P7(x971) % 47.47/47.54 [98]~P9(x981)+P7(x981) % 47.47/47.54 [99]~P2(x991)+P9(x991) % 47.47/47.54 [101]P10(x1011)+~P10(f19(x1011)) % 47.47/47.54 [103]~P5(x1031)+~P18(f10(x1031)) % 47.47/47.54 [104]~P5(x1041)+P8(f10(x1041),x1041) % 47.47/47.54 [105]~P5(x1051)+P8(f11(x1051),x1051) % 47.47/47.54 [110]P10(x1101)+P12(f19(x1101),f25(x1101)) % 47.47/47.54 [111]~P7(x1111)+P12(f23(x1111),f24(x1111)) % 47.47/47.54 [109]~P10(x1091)+~P14(x1092,x1091) % 47.47/47.54 [113]~P14(x1131,x1132)+P12(x1131,x1132) % 47.47/47.54 [117]~P14(x1172,x1171)+~P14(x1171,x1172) % 47.47/47.54 [116]~P11(x1161,x1162)+P12(x1161,f25(x1162)) % 47.47/47.54 [118]P11(x1181,x1182)+~P12(x1181,f25(x1182)) % 47.47/47.54 [102]~P5(x1021)+P18(x1021)+P13(f21(x1021)) % 47.47/47.54 [106]~P5(x1061)+P18(x1061)+~P10(f24(x1061)) % 47.47/47.54 [107]~P5(x1071)+P18(x1071)+~P10(f21(x1071)) % 47.47/47.54 [108]~P5(x1081)+P18(x1081)+~P10(f3(x1081)) % 47.47/47.54 [114]~P4(x1141)+P18(x1141)+P12(f27(x1141),f24(x1141)) % 47.47/47.54 [119]~P5(x1191)+P18(x1191)+P12(f21(x1191),f25(f24(x1191))) % 47.47/47.54 [120]~P5(x1201)+P18(x1201)+P12(f3(x1201),f25(f24(x1201))) % 47.47/47.54 [100]~P10(x1002)+~P10(x1001)+E(x1001,x1002) % 47.47/47.54 [112]~P8(x1121,x1122)+P6(x1121)+~P5(x1122) % 47.47/47.54 [115]~P12(x1152,x1151)+P10(x1151)+P14(x1152,x1151) % 47.47/47.54 [121]~P10(x1211)+~P14(x1212,x1213)+~P12(x1213,f25(x1211)) % 47.47/47.54 [122]P12(x1221,x1222)+~P14(x1221,x1223)+~P12(x1223,f25(x1222)) % 47.47/47.54 [123]P18(x1231)+~P5(x1231)+~P12(x1233,f24(x1231))+~P12(x1232,f24(x1231))+E(f28(x1231,x1232,x1233),f26(x1232,x1233)) % 47.47/47.54 [124]P18(x1241)+~P5(x1241)+~P12(x1243,f24(x1241))+~P12(x1242,f24(x1241))+E(f28(x1241,x1242,x1243),f28(x1241,x1243,x1242)) % 47.47/47.54 [125]~P5(x1251)+P18(x1251)+~P12(x1253,f24(x1251))+~P12(x1252,f24(x1251))+P13(f28(x1251,x1252,x1253)) % 47.47/47.54 [126]~P5(x1261)+P18(x1261)+~P12(x1263,f24(x1261))+~P12(x1262,f24(x1261))+P12(f28(x1261,x1262,x1263),f25(f24(x1261))) % 47.47/47.54 [128]P18(x1281)+~P8(x1282,x1281)+~P21(x1282,x1281)+~P2(x1281)+~P24(x1281)+~P23(x1281)+~P22(x1281)+~P17(x1281)+~P20(x1282)+~P20(x1281)+~P19(x1282)+~P19(x1281)+~P16(x1282)+~P16(x1281)+~P1(x1282)+~P1(x1281)+P18(x1282)+~P15(f28(x1282,x1284,x1283),x1281,x1282)+~P12(x1283,f24(x1282))+E(f27(x1281),f23(x1281))+~E(x1283,f23(x1282))+~P12(x1284,f24(x1282)) % 47.47/47.54 [129]P18(x1291)+~P8(x1292,x1291)+~P21(x1292,x1291)+~P2(x1291)+~P24(x1291)+~P23(x1291)+~P22(x1291)+~P17(x1291)+~P20(x1292)+~P20(x1291)+~P19(x1292)+~P19(x1291)+~P16(x1292)+~P16(x1291)+~P1(x1292)+~P1(x1291)+P18(x1292)+~P15(f28(x1292,x1293,x1294),x1291,x1292)+~P12(x1293,f24(x1292))+E(f27(x1291),f23(x1291))+~E(x1293,f23(x1292))+~P12(x1294,f24(x1292)) % 47.47/47.54 %EqnAxiom % 47.47/47.54 [1]E(x11,x11) % 47.47/47.54 [2]E(x22,x21)+~E(x21,x22) % 47.47/47.54 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 47.47/47.54 [4]~E(x41,x42)+E(f20(x41),f20(x42)) % 47.47/47.54 [5]~E(x51,x52)+E(f24(x51),f24(x52)) % 47.47/47.54 [6]~E(x61,x62)+E(f14(x61),f14(x62)) % 47.47/47.54 [7]~E(x71,x72)+E(f28(x71,x73,x74),f28(x72,x73,x74)) % 47.47/47.55 [8]~E(x81,x82)+E(f28(x83,x81,x84),f28(x83,x82,x84)) % 47.47/47.55 [9]~E(x91,x92)+E(f28(x93,x94,x91),f28(x93,x94,x92)) % 47.47/47.55 [10]~E(x101,x102)+E(f25(x101),f25(x102)) % 47.47/47.55 [11]~E(x111,x112)+E(f26(x111,x113),f26(x112,x113)) % 47.47/47.55 [12]~E(x121,x122)+E(f26(x123,x121),f26(x123,x122)) % 47.47/47.55 [13]~E(x131,x132)+E(f3(x131),f3(x132)) % 47.47/47.55 [14]~E(x141,x142)+E(f27(x141),f27(x142)) % 47.47/47.55 [15]~E(x151,x152)+E(f23(x151),f23(x152)) % 47.47/47.55 [16]~E(x161,x162)+E(f19(x161),f19(x162)) % 47.47/47.55 [17]~E(x171,x172)+E(f21(x171),f21(x172)) % 47.47/47.55 [18]~E(x181,x182)+E(f11(x181),f11(x182)) % 47.47/47.55 [19]~E(x191,x192)+E(f10(x191),f10(x192)) % 47.47/47.55 [20]~P1(x201)+P1(x202)+~E(x201,x202) % 47.47/47.55 [21]P15(x212,x213,x214)+~E(x211,x212)+~P15(x211,x213,x214) % 47.47/47.55 [22]P15(x223,x222,x224)+~E(x221,x222)+~P15(x223,x221,x224) % 47.47/47.55 [23]P15(x233,x234,x232)+~E(x231,x232)+~P15(x233,x234,x231) % 47.47/47.55 [24]~P16(x241)+P16(x242)+~E(x241,x242) % 47.47/47.55 [25]~P22(x251)+P22(x252)+~E(x251,x252) % 47.47/47.55 [26]~P19(x261)+P19(x262)+~E(x261,x262) % 47.47/47.55 [27]~P20(x271)+P20(x272)+~E(x271,x272) % 47.47/47.55 [28]~P23(x281)+P23(x282)+~E(x281,x282) % 47.47/47.55 [29]P12(x292,x293)+~E(x291,x292)+~P12(x291,x293) % 47.47/47.55 [30]P12(x303,x302)+~E(x301,x302)+~P12(x303,x301) % 47.47/47.55 [31]~P17(x311)+P17(x312)+~E(x311,x312) % 47.47/47.55 [32]P21(x322,x323)+~E(x321,x322)+~P21(x321,x323) % 47.47/47.55 [33]P21(x333,x332)+~E(x331,x332)+~P21(x333,x331) % 47.47/47.55 [34]~P2(x341)+P2(x342)+~E(x341,x342) % 47.47/47.55 [35]~P24(x351)+P24(x352)+~E(x351,x352) % 47.47/47.55 [36]~P5(x361)+P5(x362)+~E(x361,x362) % 47.47/47.55 [37]~P18(x371)+P18(x372)+~E(x371,x372) % 47.47/47.55 [38]~P10(x381)+P10(x382)+~E(x381,x382) % 47.47/47.55 [39]P14(x392,x393)+~E(x391,x392)+~P14(x391,x393) % 47.47/47.55 [40]P14(x403,x402)+~E(x401,x402)+~P14(x403,x401) % 47.47/47.55 [41]~P3(x411)+P3(x412)+~E(x411,x412) % 47.47/47.55 [42]~P4(x421)+P4(x422)+~E(x421,x422) % 47.47/47.55 [43]P8(x432,x433)+~E(x431,x432)+~P8(x431,x433) % 47.47/47.55 [44]P8(x443,x442)+~E(x441,x442)+~P8(x443,x441) % 47.47/47.55 [45]~P7(x451)+P7(x452)+~E(x451,x452) % 47.47/47.55 [46]~P6(x461)+P6(x462)+~E(x461,x462) % 47.47/47.55 [47]~P9(x471)+P9(x472)+~E(x471,x472) % 47.47/47.55 [48]~P13(x481)+P13(x482)+~E(x481,x482) % 47.47/47.55 [49]P11(x492,x493)+~E(x491,x492)+~P11(x491,x493) % 47.47/47.55 [50]P11(x503,x502)+~E(x501,x502)+~P11(x503,x501) % 47.47/47.55 % 47.47/47.55 %------------------------------------------- % 47.47/47.55 cnf(130,plain, % 47.47/47.55 (~P21(x1301,x1302)+~P2(x1302)+~P24(x1302)+~P23(x1302)+~P22(x1302)+~P17(x1302)+~P20(x1301)+~P20(x1302)+~P19(x1301)+~P19(x1302)+~P16(x1301)+~P16(x1302)+~P1(x1301)+~P1(x1302)+P18(x1301)+P18(x1302)+~P8(x1301,x1302)+~P15(f28(x1301,x1303,f23(x1301)),x1302,x1301)+~P12(f23(x1301),f24(x1301))+E(f27(x1302),f23(x1302))+~P12(x1303,f24(x1301))), % 47.47/47.55 inference(equality_inference,[],[128])). % 47.47/47.55 cnf(131,plain, % 47.47/47.55 (~P21(x1311,x1312)+~P2(x1312)+~P24(x1312)+~P23(x1312)+~P22(x1312)+~P17(x1312)+~P20(x1311)+~P20(x1312)+~P19(x1311)+~P19(x1312)+~P16(x1311)+~P16(x1312)+~P1(x1311)+~P1(x1312)+P18(x1311)+P18(x1312)+~P8(x1311,x1312)+~P15(f28(x1311,f23(x1311),x1313),x1312,x1311)+~P12(f23(x1311),f24(x1311))+E(f27(x1312),f23(x1312))+~P12(x1313,f24(x1311))), % 47.47/47.55 inference(equality_inference,[],[129])). % 47.47/47.55 cnf(135,plain, % 47.47/47.55 (P12(f14(x1351),x1351)), % 47.47/47.55 inference(rename_variables,[],[80])). % 47.47/47.55 cnf(137,plain, % 47.47/47.55 (P14(f14(a22),a22)), % 47.47/47.55 inference(scs_inference,[],[80,135,65,87,109,118,115])). % 47.47/47.55 cnf(162,plain, % 47.47/47.55 (~P14(x1621,f14(f25(a16)))), % 47.47/47.55 inference(scs_inference,[],[80,82,81,66,118,109,50,121])). % 47.47/47.55 cnf(291,plain, % 47.47/47.55 (~P15(f28(a12,f23(a12),a18),a1,a12)+~P7(a12)), % 47.47/47.55 inference(scs_inference,[],[51,76,77,88,79,52,54,56,58,84,53,55,59,60,61,62,63,83,57,137,162,40,131,111])). % 47.47/47.55 cnf(308,plain, % 47.47/47.55 (~P15(f28(a12,a18,f23(a12)),a1,a12)+~P7(a12)), % 47.47/47.55 inference(scs_inference,[],[51,76,77,79,88,52,54,56,58,84,53,55,59,60,61,62,63,83,57,130,113,111])). % 47.47/47.55 cnf(326,plain, % 47.47/47.55 (P7(a1)), % 47.47/47.55 inference(scs_inference,[],[63,96,97])). % 47.47/47.55 cnf(3817,plain, % 47.47/47.55 (~P7(a12)+P15(f28(a12,a18,f23(a12)),a1,a12)), % 47.47/47.55 inference(scs_inference,[],[291,127])). % 47.47/47.55 cnf(3905,plain, % 47.47/47.55 (~P7(a12)), % 47.47/47.55 inference(scs_inference,[],[308,3817])). % 47.47/47.55 cnf(3914,plain, % 47.47/47.55 ($false), % 47.47/47.55 inference(scs_inference,[],[77,3905,326,98,97,112,96,95]), % 47.47/47.55 ['proof']). % 47.47/47.55 % SZS output end Proof % 47.47/47.55 % Total time :46.910000s %------------------------------------------------------------------------------