%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : RNG112+4 : TPTP v8.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/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 14:01:08 EDT 2024 % Result : Theorem 69.89s 69.89s % Output : CNFRefutation 69.89s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.13 % Problem : RNG112+4 : TPTP v8.2.0. Released v4.0.0. % 0.04/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n018.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 13:15:38 EDT 2024 % 0.12/0.34 % CPUTime : % 0.56/0.58 start to proof:theBenchmark % 69.79/69.87 %------------------------------------------- % 69.79/69.87 % File :CSE---1.7 % 69.79/69.87 % Problem :theBenchmark % 69.79/69.87 % Transform :cnf % 69.79/69.87 % Format :tptp:raw % 69.79/69.87 % Command :java -jar mcs_scs.jar %d %s % 69.79/69.87 % 69.79/69.87 % Result :Theorem 69.200000s % 69.79/69.87 % Output :CNFRefutation 69.200000s % 69.79/69.87 %------------------------------------------- % 69.79/69.88 %------------------------------------------------------------------------------ % 69.79/69.88 % File : RNG112+4 : TPTP v8.2.0. Released v4.0.0. % 69.79/69.88 % Domain : Ring Theory % 69.79/69.88 % Problem : Chinese remainder theorem in a ring 07_04_02, 03 expansion % 69.79/69.88 % Version : Especial. % 69.79/69.88 % English : % 69.79/69.88 % 69.79/69.88 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 69.79/69.88 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 69.79/69.88 % Source : [Pas08] % 69.79/69.88 % Names : chines_07_04_02.03 [Pas08] % 69.79/69.88 % 69.79/69.88 % Status : Theorem % 69.79/69.88 % Rating : 0.39 v8.2.0, 0.36 v8.1.0, 0.31 v7.5.0, 0.34 v7.4.0, 0.37 v7.3.0, 0.38 v7.2.0, 0.34 v7.1.0, 0.39 v7.0.0, 0.33 v6.4.0, 0.38 v6.3.0, 0.42 v6.2.0, 0.40 v6.1.0, 0.47 v6.0.0, 0.43 v5.5.0, 0.52 v5.4.0, 0.54 v5.3.0, 0.56 v5.2.0, 0.40 v5.1.0, 0.48 v5.0.0, 0.62 v4.1.0, 0.65 v4.0.1, 0.87 v4.0.0 % 69.79/69.88 % Syntax : Number of formulae : 46 ( 3 unt; 9 def) % 69.79/69.88 % Number of atoms : 247 ( 60 equ) % 69.79/69.88 % Maximal formula atoms : 23 ( 5 avg) % 69.79/69.88 % Number of connectives : 215 ( 14 ~; 9 |; 120 &) % 69.79/69.88 % ( 17 <=>; 55 =>; 0 <=; 0 <~>) % 69.79/69.88 % Maximal formula depth : 18 ( 7 avg) % 69.79/69.88 % Maximal term depth : 3 ( 1 avg) % 69.79/69.88 % Number of predicates : 13 ( 11 usr; 1 prp; 0-3 aty) % 69.79/69.88 % Number of functors : 13 ( 13 usr; 6 con; 0-2 aty) % 69.79/69.88 % Number of variables : 126 ( 89 !; 37 ?) % 69.79/69.88 % SPC : FOF_THM_RFO_SEQ % 69.79/69.88 % 69.79/69.88 % Comments : Problem generated by the SAD system [VLP07] % 69.79/69.88 %------------------------------------------------------------------------------ % 69.79/69.88 fof(mElmSort,axiom, % 69.79/69.88 ! [W0] : % 69.79/69.88 ( aElement0(W0) % 69.79/69.88 => $true ) ). % 69.79/69.88 % 69.79/69.88 fof(mSortsC,axiom, % 69.79/69.88 aElement0(sz00) ). % 69.79/69.88 % 69.79/69.88 fof(mSortsC_01,axiom, % 69.79/69.88 aElement0(sz10) ). % 69.79/69.88 % 69.79/69.88 fof(mSortsU,axiom, % 69.79/69.88 ! [W0] : % 69.79/69.88 ( aElement0(W0) % 69.79/69.88 => aElement0(smndt0(W0)) ) ). % 69.79/69.88 % 69.79/69.88 fof(mSortsB,axiom, % 69.79/69.88 ! [W0,W1] : % 69.79/69.88 ( ( aElement0(W0) % 69.79/69.88 & aElement0(W1) ) % 69.79/69.88 => aElement0(sdtpldt0(W0,W1)) ) ). % 69.79/69.88 % 69.79/69.88 fof(mSortsB_02,axiom, % 69.79/69.88 ! [W0,W1] : % 69.79/69.88 ( ( aElement0(W0) % 69.79/69.88 & aElement0(W1) ) % 69.79/69.88 => aElement0(sdtasdt0(W0,W1)) ) ). % 69.79/69.88 % 69.79/69.88 fof(mAddComm,axiom, % 69.79/69.88 ! [W0,W1] : % 69.79/69.88 ( ( aElement0(W0) % 69.79/69.88 & aElement0(W1) ) % 69.79/69.88 => sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) ). % 69.79/69.88 % 69.79/69.88 fof(mAddAsso,axiom, % 69.79/69.88 ! [W0,W1,W2] : % 69.79/69.88 ( ( aElement0(W0) % 69.79/69.88 & aElement0(W1) % 69.79/69.88 & aElement0(W2) ) % 69.79/69.88 => sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2)) ) ). % 69.79/69.88 % 69.79/69.88 fof(mAddZero,axiom, % 69.79/69.88 ! [W0] : % 69.79/69.88 ( aElement0(W0) % 69.79/69.88 => ( sdtpldt0(W0,sz00) = W0 % 69.79/69.88 & W0 = sdtpldt0(sz00,W0) ) ) ). % 69.79/69.88 % 69.79/69.88 fof(mAddInvr,axiom, % 69.79/69.88 ! [W0] : % 69.79/69.88 ( aElement0(W0) % 69.79/69.88 => ( sdtpldt0(W0,smndt0(W0)) = sz00 % 69.79/69.88 & sz00 = sdtpldt0(smndt0(W0),W0) ) ) ). % 69.79/69.88 % 69.79/69.88 fof(mMulComm,axiom, % 69.79/69.88 ! [W0,W1] : % 69.79/69.88 ( ( aElement0(W0) % 69.79/69.88 & aElement0(W1) ) % 69.79/69.88 => sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) ). % 69.79/69.88 % 69.79/69.88 fof(mMulAsso,axiom, % 69.79/69.88 ! [W0,W1,W2] : % 69.79/69.88 ( ( aElement0(W0) % 69.79/69.88 & aElement0(W1) % 69.79/69.88 & aElement0(W2) ) % 69.79/69.88 => sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2)) ) ). % 69.79/69.88 % 69.79/69.88 fof(mMulUnit,axiom, % 69.79/69.88 ! [W0] : % 69.79/69.88 ( aElement0(W0) % 69.79/69.88 => ( sdtasdt0(W0,sz10) = W0 % 69.79/69.88 & W0 = sdtasdt0(sz10,W0) ) ) ). % 69.79/69.88 % 69.79/69.88 fof(mAMDistr,axiom, % 69.79/69.88 ! [W0,W1,W2] : % 69.79/69.88 ( ( aElement0(W0) % 69.79/69.88 & aElement0(W1) % 69.79/69.88 & aElement0(W2) ) % 69.79/69.88 => ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 69.79/69.88 & sdtasdt0(sdtpldt0(W1,W2),W0) = sdtpldt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)) ) ) ). % 69.79/69.88 % 69.79/69.88 fof(mMulMnOne,axiom, % 69.79/69.88 ! [W0] : % 69.79/69.88 ( aElement0(W0) % 69.79/69.88 => ( sdtasdt0(smndt0(sz10),W0) = smndt0(W0) % 69.79/69.88 & smndt0(W0) = sdtasdt0(W0,smndt0(sz10)) ) ) ). % 69.79/69.88 % 69.79/69.88 fof(mMulZero,axiom, % 69.79/69.88 ! [W0] : % 69.79/69.88 ( aElement0(W0) % 69.79/69.88 => ( sdtasdt0(W0,sz00) = sz00 % 69.79/69.88 & sz00 = sdtasdt0(sz00,W0) ) ) ). % 69.79/69.88 % 69.79/69.88 fof(mCancel,axiom, % 69.79/69.88 ! [W0,W1] : % 69.79/69.88 ( ( aElement0(W0) % 69.79/69.88 & aElement0(W1) ) % 69.79/69.88 => ( sdtasdt0(W0,W1) = sz00 % 69.79/69.88 => ( W0 = sz00 % 69.79/69.88 | W1 = sz00 ) ) ) ). % 69.79/69.88 % 69.79/69.88 fof(mUnNeZr,axiom, % 69.79/69.88 sz10 != sz00 ). % 69.79/69.88 % 69.79/69.88 fof(mSetSort,axiom, % 69.79/69.88 ! [W0] : % 69.79/69.88 ( aSet0(W0) % 69.79/69.88 => $true ) ). % 69.79/69.88 % 69.79/69.88 fof(mEOfElem,axiom, % 69.79/69.88 ! [W0] : % 69.79/69.88 ( aSet0(W0) % 69.79/69.88 => ! [W1] : % 69.79/69.88 ( aElementOf0(W1,W0) % 69.79/69.88 => aElement0(W1) ) ) ). % 69.79/69.88 % 69.79/69.88 fof(mSetEq,axiom, % 69.79/69.88 ! [W0,W1] : % 69.79/69.88 ( ( aSet0(W0) % 69.79/69.88 & aSet0(W1) ) % 69.79/69.88 => ( ( ! [W2] : % 69.79/69.88 ( aElementOf0(W2,W0) % 69.79/69.88 => aElementOf0(W2,W1) ) % 69.79/69.88 & ! [W2] : % 69.79/69.88 ( aElementOf0(W2,W1) % 69.79/69.88 => aElementOf0(W2,W0) ) ) % 69.79/69.88 => W0 = W1 ) ) ). % 69.79/69.88 % 69.79/69.88 fof(mDefSSum,definition, % 69.79/69.88 ! [W0,W1] : % 69.79/69.88 ( ( aSet0(W0) % 69.79/69.88 & aSet0(W1) ) % 69.79/69.88 => ! [W2] : % 69.79/69.88 ( W2 = sdtpldt1(W0,W1) % 69.79/69.88 <=> ( aSet0(W2) % 69.79/69.88 & ! [W3] : % 69.79/69.88 ( aElementOf0(W3,W2) % 69.79/69.88 <=> ? [W4,W5] : % 69.79/69.88 ( aElementOf0(W4,W0) % 69.79/69.88 & aElementOf0(W5,W1) % 69.79/69.88 & sdtpldt0(W4,W5) = W3 ) ) ) ) ) ). % 69.79/69.88 % 69.79/69.88 fof(mDefSInt,definition, % 69.79/69.88 ! [W0,W1] : % 69.79/69.88 ( ( aSet0(W0) % 69.79/69.88 & aSet0(W1) ) % 69.79/69.88 => ! [W2] : % 69.79/69.88 ( W2 = sdtasasdt0(W0,W1) % 69.79/69.88 <=> ( aSet0(W2) % 69.79/69.88 & ! [W3] : % 69.79/69.88 ( aElementOf0(W3,W2) % 69.79/69.88 <=> ( aElementOf0(W3,W0) % 69.79/69.88 & aElementOf0(W3,W1) ) ) ) ) ) ). % 69.79/69.88 % 69.79/69.88 fof(mDefIdeal,definition, % 69.79/69.88 ! [W0] : % 69.79/69.88 ( aIdeal0(W0) % 69.79/69.88 <=> ( aSet0(W0) % 69.79/69.88 & ! [W1] : % 69.79/69.88 ( aElementOf0(W1,W0) % 69.79/69.88 => ( ! [W2] : % 69.79/69.88 ( aElementOf0(W2,W0) % 69.79/69.88 => aElementOf0(sdtpldt0(W1,W2),W0) ) % 69.79/69.88 & ! [W2] : % 69.79/69.88 ( aElement0(W2) % 69.79/69.88 => aElementOf0(sdtasdt0(W2,W1),W0) ) ) ) ) ) ). % 69.79/69.88 % 69.79/69.88 fof(mIdeSum,axiom, % 69.79/69.88 ! [W0,W1] : % 69.79/69.88 ( ( aIdeal0(W0) % 69.79/69.88 & aIdeal0(W1) ) % 69.79/69.88 => aIdeal0(sdtpldt1(W0,W1)) ) ). % 69.79/69.88 % 69.79/69.88 fof(mIdeInt,axiom, % 69.79/69.88 ! [W0,W1] : % 69.79/69.88 ( ( aIdeal0(W0) % 69.79/69.88 & aIdeal0(W1) ) % 69.79/69.88 => aIdeal0(sdtasasdt0(W0,W1)) ) ). % 69.79/69.88 % 69.79/69.88 fof(mDefMod,definition, % 69.89/69.88 ! [W0,W1,W2] : % 69.89/69.88 ( ( aElement0(W0) % 69.89/69.88 & aElement0(W1) % 69.89/69.88 & aIdeal0(W2) ) % 69.89/69.88 => ( sdteqdtlpzmzozddtrp0(W0,W1,W2) % 69.89/69.88 <=> aElementOf0(sdtpldt0(W0,smndt0(W1)),W2) ) ) ). % 69.89/69.88 % 69.89/69.88 fof(mChineseRemainder,axiom, % 69.89/69.88 ! [W0,W1] : % 69.89/69.88 ( ( aIdeal0(W0) % 69.89/69.88 & aIdeal0(W1) ) % 69.89/69.88 => ( ! [W2] : % 69.89/69.88 ( aElement0(W2) % 69.89/69.88 => aElementOf0(W2,sdtpldt1(W0,W1)) ) % 69.89/69.88 => ! [W2,W3] : % 69.89/69.88 ( ( aElement0(W2) % 69.89/69.88 & aElement0(W3) ) % 69.89/69.88 => ? [W4] : % 69.89/69.88 ( aElement0(W4) % 69.89/69.88 & sdteqdtlpzmzozddtrp0(W4,W2,W0) % 69.89/69.88 & sdteqdtlpzmzozddtrp0(W4,W3,W1) ) ) ) ) ). % 69.89/69.88 % 69.89/69.88 fof(mNatSort,axiom, % 69.89/69.88 ! [W0] : % 69.89/69.88 ( aNaturalNumber0(W0) % 69.89/69.88 => $true ) ). % 69.89/69.88 % 69.89/69.88 fof(mEucSort,axiom, % 69.89/69.88 ! [W0] : % 69.89/69.88 ( ( aElement0(W0) % 69.89/69.88 & W0 != sz00 ) % 69.89/69.88 => aNaturalNumber0(sbrdtbr0(W0)) ) ). % 69.89/69.88 % 69.89/69.88 fof(mNatLess,axiom, % 69.89/69.88 ! [W0,W1] : % 69.89/69.88 ( ( aNaturalNumber0(W0) % 69.89/69.88 & aNaturalNumber0(W1) ) % 69.89/69.88 => ( iLess0(W0,W1) % 69.89/69.88 => $true ) ) ). % 69.89/69.88 % 69.89/69.88 fof(mDivision,axiom, % 69.89/69.88 ! [W0,W1] : % 69.89/69.88 ( ( aElement0(W0) % 69.89/69.88 & aElement0(W1) % 69.89/69.88 & W1 != sz00 ) % 69.89/69.88 => ? [W2,W3] : % 69.89/69.88 ( aElement0(W2) % 69.89/69.88 & aElement0(W3) % 69.89/69.88 & W0 = sdtpldt0(sdtasdt0(W2,W1),W3) % 69.89/69.88 & ( W3 != sz00 % 69.89/69.88 => iLess0(sbrdtbr0(W3),sbrdtbr0(W1)) ) ) ) ). % 69.89/69.88 % 69.89/69.88 fof(mDefDiv,definition, % 69.89/69.88 ! [W0,W1] : % 69.89/69.88 ( ( aElement0(W0) % 69.89/69.88 & aElement0(W1) ) % 69.89/69.89 => ( doDivides0(W0,W1) % 69.89/69.89 <=> ? [W2] : % 69.89/69.89 ( aElement0(W2) % 69.89/69.89 & sdtasdt0(W0,W2) = W1 ) ) ) ). % 69.89/69.89 % 69.89/69.89 fof(mDefDvs,definition, % 69.89/69.89 ! [W0] : % 69.89/69.89 ( aElement0(W0) % 69.89/69.89 => ! [W1] : % 69.89/69.89 ( aDivisorOf0(W1,W0) % 69.89/69.89 <=> ( aElement0(W1) % 69.89/69.89 & doDivides0(W1,W0) ) ) ) ). % 69.89/69.89 % 69.89/69.89 fof(mDefGCD,definition, % 69.89/69.89 ! [W0,W1] : % 69.89/69.89 ( ( aElement0(W0) % 69.89/69.89 & aElement0(W1) ) % 69.89/69.89 => ! [W2] : % 69.89/69.89 ( aGcdOfAnd0(W2,W0,W1) % 69.89/69.89 <=> ( aDivisorOf0(W2,W0) % 69.89/69.89 & aDivisorOf0(W2,W1) % 69.89/69.89 & ! [W3] : % 69.89/69.89 ( ( aDivisorOf0(W3,W0) % 69.89/69.89 & aDivisorOf0(W3,W1) ) % 69.89/69.89 => doDivides0(W3,W2) ) ) ) ) ). % 69.89/69.89 % 69.89/69.89 fof(mDefRel,definition, % 69.89/69.89 ! [W0,W1] : % 69.89/69.89 ( ( aElement0(W0) % 69.89/69.89 & aElement0(W1) ) % 69.89/69.89 => ( misRelativelyPrime0(W0,W1) % 69.89/69.89 <=> aGcdOfAnd0(sz10,W0,W1) ) ) ). % 69.89/69.89 % 69.89/69.89 fof(mDefPrIdeal,definition, % 69.89/69.89 ! [W0] : % 69.89/69.89 ( aElement0(W0) % 69.89/69.89 => ! [W1] : % 69.89/69.89 ( W1 = slsdtgt0(W0) % 69.89/69.89 <=> ( aSet0(W1) % 69.89/69.89 & ! [W2] : % 69.89/69.89 ( aElementOf0(W2,W1) % 69.89/69.89 <=> ? [W3] : % 69.89/69.89 ( aElement0(W3) % 69.89/69.89 & sdtasdt0(W0,W3) = W2 ) ) ) ) ) ). % 69.89/69.89 % 69.89/69.89 fof(mPrIdeal,axiom, % 69.89/69.89 ! [W0] : % 69.89/69.89 ( aElement0(W0) % 69.89/69.89 => aIdeal0(slsdtgt0(W0)) ) ). % 69.89/69.89 % 69.89/69.89 fof(m__2091,hypothesis, % 69.89/69.89 ( aElement0(xa) % 69.89/69.89 & aElement0(xb) ) ). % 69.89/69.89 % 69.89/69.89 fof(m__2110,hypothesis, % 69.89/69.89 ( xa != sz00 % 69.89/69.89 | xb != sz00 ) ). % 69.89/69.89 % 69.89/69.89 fof(m__2129,hypothesis, % 69.89/69.89 ( aElement0(xc) % 69.89/69.89 & ? [W0] : % 69.89/69.89 ( aElement0(W0) % 69.89/69.89 & sdtasdt0(xc,W0) = xa ) % 69.89/69.89 & doDivides0(xc,xa) % 69.89/69.89 & aDivisorOf0(xc,xa) % 69.89/69.89 & aElement0(xc) % 69.89/69.89 & ? [W0] : % 69.89/69.89 ( aElement0(W0) % 69.89/69.89 & sdtasdt0(xc,W0) = xb ) % 69.89/69.89 & doDivides0(xc,xb) % 69.89/69.89 & aDivisorOf0(xc,xb) % 69.89/69.89 & ! [W0] : % 69.89/69.89 ( ( ( ( aElement0(W0) % 69.89/69.89 & ( ? [W1] : % 69.89/69.89 ( aElement0(W1) % 69.89/69.89 & sdtasdt0(W0,W1) = xa ) % 69.89/69.89 | doDivides0(W0,xa) ) ) % 69.89/69.89 | aDivisorOf0(W0,xa) ) % 69.89/69.89 & ( ? [W1] : % 69.89/69.89 ( aElement0(W1) % 69.89/69.89 & sdtasdt0(W0,W1) = xb ) % 69.89/69.89 | doDivides0(W0,xb) % 69.89/69.89 | aDivisorOf0(W0,xb) ) ) % 69.89/69.89 => ( ? [W1] : % 69.89/69.89 ( aElement0(W1) % 69.89/69.89 & sdtasdt0(W0,W1) = xc ) % 69.89/69.89 & doDivides0(W0,xc) ) ) % 69.89/69.89 & aGcdOfAnd0(xc,xa,xb) ) ). % 69.89/69.89 % 69.89/69.89 fof(m__2174,hypothesis, % 69.89/69.89 ( aSet0(xI) % 69.89/69.89 & ! [W0] : % 69.89/69.89 ( aElementOf0(W0,xI) % 69.89/69.89 => ( ! [W1] : % 69.89/69.89 ( aElementOf0(W1,xI) % 69.89/69.89 => aElementOf0(sdtpldt0(W0,W1),xI) ) % 69.89/69.89 & ! [W1] : % 69.89/69.89 ( aElement0(W1) % 69.89/69.89 => aElementOf0(sdtasdt0(W1,W0),xI) ) ) ) % 69.89/69.89 & aIdeal0(xI) % 69.89/69.89 & ! [W0] : % 69.89/69.89 ( aElementOf0(W0,slsdtgt0(xa)) % 69.89/69.89 <=> ? [W1] : % 69.89/69.89 ( aElement0(W1) % 69.89/69.89 & sdtasdt0(xa,W1) = W0 ) ) % 69.89/69.89 & ! [W0] : % 69.89/69.89 ( aElementOf0(W0,slsdtgt0(xb)) % 69.89/69.89 <=> ? [W1] : % 69.89/69.89 ( aElement0(W1) % 69.89/69.89 & sdtasdt0(xb,W1) = W0 ) ) % 69.89/69.89 & ! [W0] : % 69.89/69.89 ( aElementOf0(W0,xI) % 69.89/69.89 <=> ? [W1,W2] : % 69.89/69.89 ( aElementOf0(W1,slsdtgt0(xa)) % 69.89/69.89 & aElementOf0(W2,slsdtgt0(xb)) % 69.89/69.89 & sdtpldt0(W1,W2) = W0 ) ) % 69.89/69.89 & xI = sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)) ) ). % 69.89/69.89 % 69.89/69.89 fof(m__2203,hypothesis, % 69.89/69.89 ( ? [W0] : % 69.89/69.89 ( aElement0(W0) % 69.89/69.89 & sdtasdt0(xa,W0) = sz00 ) % 69.89/69.89 & aElementOf0(sz00,slsdtgt0(xa)) % 69.89/69.89 & ? [W0] : % 69.89/69.89 ( aElement0(W0) % 69.89/69.89 & sdtasdt0(xa,W0) = xa ) % 69.89/69.89 & aElementOf0(xa,slsdtgt0(xa)) % 69.89/69.89 & ? [W0] : % 69.89/69.89 ( aElement0(W0) % 69.89/69.89 & sdtasdt0(xb,W0) = sz00 ) % 69.89/69.89 & aElementOf0(sz00,slsdtgt0(xb)) % 69.89/69.89 & ? [W0] : % 69.89/69.89 ( aElement0(W0) % 69.89/69.89 & sdtasdt0(xb,W0) = xb ) % 69.89/69.89 & aElementOf0(xb,slsdtgt0(xb)) ) ). % 69.89/69.89 % 69.89/69.89 fof(m__2228,hypothesis, % 69.89/69.89 ? [W0] : % 69.89/69.89 ( ! [W1] : % 69.89/69.89 ( aElementOf0(W1,slsdtgt0(xa)) % 69.89/69.89 <=> ? [W2] : % 69.89/69.89 ( aElement0(W2) % 69.89/69.89 & sdtasdt0(xa,W2) = W1 ) ) % 69.89/69.89 & ! [W1] : % 69.89/69.89 ( aElementOf0(W1,slsdtgt0(xb)) % 69.89/69.89 <=> ? [W2] : % 69.89/69.89 ( aElement0(W2) % 69.89/69.89 & sdtasdt0(xb,W2) = W1 ) ) % 69.89/69.89 & ? [W1,W2] : % 69.89/69.89 ( aElementOf0(W1,slsdtgt0(xa)) % 69.89/69.89 & aElementOf0(W2,slsdtgt0(xb)) % 69.89/69.89 & sdtpldt0(W1,W2) = W0 ) % 69.89/69.89 & aElementOf0(W0,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))) % 69.89/69.89 & W0 != sz00 ) ). % 69.89/69.89 % 69.89/69.89 fof(m__2351,hypothesis, % 69.89/69.89 ! [W0] : % 69.89/69.89 ( ( ( ? [W1,W2] : % 69.89/69.89 ( aElementOf0(W1,slsdtgt0(xa)) % 69.89/69.89 & aElementOf0(W2,slsdtgt0(xb)) % 69.89/69.89 & sdtpldt0(W1,W2) = W0 ) % 69.89/69.89 | aElementOf0(W0,xI) ) % 69.89/69.89 & W0 != sz00 ) % 69.89/69.89 => ? [W1] : % 69.89/69.89 ( ? [W2,W3] : % 69.89/69.89 ( aElementOf0(W2,slsdtgt0(xa)) % 69.89/69.89 & aElementOf0(W3,slsdtgt0(xb)) % 69.89/69.89 & sdtpldt0(W2,W3) = W1 ) % 69.89/69.89 & aElementOf0(W1,xI) % 69.89/69.89 & W1 != sz00 % 69.89/69.89 & ! [W2] : % 69.89/69.89 ( ( ( ? [W3,W4] : % 69.89/69.89 ( aElementOf0(W3,slsdtgt0(xa)) % 69.89/69.89 & aElementOf0(W4,slsdtgt0(xb)) % 69.89/69.89 & sdtpldt0(W3,W4) = W2 ) % 69.89/69.89 | aElementOf0(W2,xI) ) % 69.89/69.89 & W2 != sz00 ) % 69.89/69.89 => ~ iLess0(sbrdtbr0(W2),sbrdtbr0(W1)) ) ) ) ). % 69.89/69.89 % 69.89/69.89 fof(m__,conjecture, % 69.89/69.89 ? [W0] : % 69.89/69.89 ( ( ? [W1,W2] : % 69.89/69.89 ( aElementOf0(W1,slsdtgt0(xa)) % 69.89/69.89 & aElementOf0(W2,slsdtgt0(xb)) % 69.89/69.89 & sdtpldt0(W1,W2) = W0 ) % 69.89/69.89 | aElementOf0(W0,xI) ) % 69.89/69.89 & W0 != sz00 % 69.89/69.89 & ! [W1] : % 69.89/69.89 ( ( ? [W2,W3] : % 69.89/69.89 ( aElementOf0(W2,slsdtgt0(xa)) % 69.89/69.89 & aElementOf0(W3,slsdtgt0(xb)) % 69.89/69.89 & sdtpldt0(W2,W3) = W1 ) % 69.89/69.89 & aElementOf0(W1,xI) % 69.89/69.89 & W1 != sz00 ) % 69.89/69.89 => ~ iLess0(sbrdtbr0(W1),sbrdtbr0(W0)) ) ) ). % 69.89/69.89 % 69.89/69.89 %------------------------------------------------------------------------------ % 69.89/69.89 %------------------------------------------- % 69.89/69.89 % Proof found % 69.89/69.89 % SZS status Theorem for theBenchmark % 69.89/69.89 % SZS output start Proof % 69.89/69.89 %ClaNum:287(EqnAxiom:93) % 69.89/69.89 %VarNum:1028(SingletonVarNum:336) % 69.89/69.89 %MaxLitNum:9 % 69.89/69.89 %MaxfuncDepth:2 % 69.89/69.89 %SharedTerms:73 % 69.89/69.89 %goalClause: 147 160 173 174 189 195 227 238 241 242 244 249 % 69.89/69.89 [94]P1(a1) % 69.89/69.89 [95]P1(a51) % 69.89/69.89 [96]P1(a52) % 69.89/69.89 [97]P1(a54) % 69.89/69.89 [99]P1(a55) % 69.89/69.89 [100]P1(a2) % 69.89/69.89 [101]P1(a15) % 69.89/69.89 [102]P1(a16) % 69.89/69.89 [103]P1(a22) % 69.89/69.89 [104]P1(a23) % 69.89/69.89 [105]P1(a25) % 69.89/69.89 [106]P3(a53) % 69.89/69.89 [107]P4(a53) % 69.89/69.89 [115]P8(a55,a52) % 69.89/69.89 [116]P8(a55,a54) % 69.89/69.89 [117]P2(a55,a52) % 69.89/69.89 [118]P2(a55,a54) % 69.89/69.89 [126]P6(a55,a52,a54) % 69.89/69.89 [128]~E(a1,a51) % 69.89/69.89 [129]~E(a1,a27) % 69.89/69.89 [108]E(f31(a26,a30),a27) % 69.89/69.89 [109]E(f32(a52,a16),a1) % 69.89/69.89 [110]E(f32(a52,a22),a52) % 69.89/69.89 [111]E(f32(a54,a23),a1) % 69.89/69.89 [112]E(f32(a54,a25),a54) % 69.89/69.89 [113]E(f32(a55,a2),a52) % 69.89/69.89 [114]E(f32(a55,a15),a54) % 69.89/69.89 [119]P5(a1,f48(a52)) % 69.89/69.89 [120]P5(a1,f48(a54)) % 69.89/69.89 [121]P5(a52,f48(a52)) % 69.89/69.89 [122]P5(a54,f48(a54)) % 69.89/69.89 [123]P5(a26,f48(a52)) % 69.89/69.89 [124]P5(a30,f48(a54)) % 69.89/69.89 [125]E(f49(f48(a52),f48(a54)),a53) % 69.89/69.89 [127]P5(a27,f49(f48(a52),f48(a54))) % 69.89/69.89 [130]~E(a1,a52)+~E(a1,a54) % 69.89/69.89 [131]~P4(x1311)+P3(x1311) % 69.89/69.89 [132]~P1(x1321)+P1(f50(x1321)) % 69.89/69.89 [133]~P1(x1331)+P4(f48(x1331)) % 69.89/69.89 [135]~P1(x1351)+E(f32(a1,x1351),a1) % 69.89/69.89 [136]~P1(x1361)+E(f32(x1361,a1),a1) % 69.89/69.89 [138]~P1(x1381)+E(f31(a1,x1381),x1381) % 69.89/69.89 [139]~P1(x1391)+E(f32(a51,x1391),x1391) % 69.89/69.89 [140]~P1(x1401)+E(f31(x1401,a1),x1401) % 69.89/69.89 [141]~P1(x1411)+E(f32(x1411,a51),x1411) % 69.89/69.89 [155]~P5(x1551,f48(a52))+P1(f17(x1551)) % 69.89/69.89 [156]~P5(x1561,f48(a54))+P1(f19(x1561)) % 69.89/69.89 [157]~P5(x1571,f48(a52))+P1(f28(x1571)) % 69.89/69.89 [158]~P5(x1581,f48(a54))+P1(f29(x1581)) % 69.89/69.89 [166]~P5(x1661,a53)+P5(f20(x1661),f48(a52)) % 69.89/69.89 [167]~P5(x1671,a53)+P5(f21(x1671),f48(a54)) % 69.89/69.89 [143]~P1(x1431)+E(f31(f50(x1431),x1431),a1) % 69.89/69.89 [144]~P1(x1441)+E(f31(x1441,f50(x1441)),a1) % 69.89/69.89 [145]~P1(x1451)+E(f32(x1451,f50(a51)),f50(x1451)) % 69.89/69.89 [146]~P1(x1461)+E(f32(f50(a51),x1461),f50(x1461)) % 69.89/69.89 [181]~P5(x1811,f48(a52))+E(f32(a52,f17(x1811)),x1811) % 69.89/69.89 [182]~P5(x1821,f48(a52))+E(f32(a52,f28(x1821)),x1821) % 69.89/69.89 [183]~P5(x1831,f48(a54))+E(f32(a54,f19(x1831)),x1831) % 69.89/69.89 [184]~P5(x1841,f48(a54))+E(f32(a54,f29(x1841)),x1841) % 69.89/69.89 [185]~P5(x1851,a53)+E(f31(f20(x1851),f21(x1851)),x1851) % 69.89/69.89 [142]~P5(x1421,a53)+E(x1421,a1)+~E(a34,a1) % 69.89/69.89 [150]~P5(x1501,a53)+E(x1501,a1)+P5(a34,a53) % 69.89/69.89 [190]~P8(x1901,a54)+~P2(x1901,a52)+P8(x1901,a55) % 69.89/69.89 [191]~P2(x1911,a52)+~P2(x1911,a54)+P8(x1911,a55) % 69.89/69.89 [134]~P1(x1341)+E(x1341,a1)+P7(f33(x1341)) % 69.89/69.89 [147]~P5(x1471,a53)+E(x1471,a1)+~E(f35(x1471),a1) % 69.89/69.89 [148]~P3(x1481)+P4(x1481)+P5(f39(x1481),x1481) % 69.89/69.89 [149]~P5(x1491,a53)+E(x1491,a1)+E(f31(a36,a37),a34) % 69.89/69.89 [153]~P5(x1531,a53)+E(x1531,a1)+P5(a36,f48(a52)) % 69.89/69.89 [154]~P5(x1541,a53)+E(x1541,a1)+P5(a37,f48(a54)) % 69.89/69.89 [160]~P5(x1601,a53)+E(x1601,a1)+P5(f35(x1601),a53) % 69.89/69.89 [173]~P5(x1731,a53)+E(x1731,a1)+P5(f40(x1731),f48(a52)) % 69.89/69.89 [174]~P5(x1741,a53)+E(x1741,a1)+P5(f41(x1741),f48(a54)) % 69.89/69.89 [186]~P8(x1861,a54)+~P2(x1861,a52)+P1(f18(x1861)) % 69.89/69.89 [187]~P2(x1871,a52)+~P2(x1871,a54)+P1(f18(x1871)) % 69.89/69.89 [189]~P5(x1891,a53)+E(x1891,a1)+E(f31(f40(x1891),f41(x1891)),f35(x1891)) % 69.89/69.89 [195]~P5(x1951,a53)+E(x1951,a1)+P9(f33(f35(x1951)),f33(x1951)) % 69.89/69.89 [200]~P8(x2001,a54)+~P2(x2001,a52)+E(f32(x2001,f18(x2001)),a55) % 69.89/69.89 [201]~P2(x2011,a52)+~P2(x2011,a54)+E(f32(x2011,f18(x2011)),a55) % 69.89/69.89 [151]~P5(x1511,x1512)+P1(x1511)+~P3(x1512) % 69.89/69.89 [152]~P2(x1521,x1522)+P1(x1521)+~P1(x1522) % 69.89/69.89 [168]~P1(x1682)+~P2(x1681,x1682)+P8(x1681,x1682) % 69.89/69.89 [137]~P1(x1372)+P3(x1371)+~E(x1371,f48(x1372)) % 69.89/69.89 [161]~P1(x1612)+~P1(x1611)+E(f31(x1611,x1612),f31(x1612,x1611)) % 69.89/69.89 [162]~P1(x1622)+~P1(x1621)+E(f32(x1621,x1622),f32(x1622,x1621)) % 69.89/69.89 [169]~P1(x1692)+~P1(x1691)+P1(f31(x1691,x1692)) % 69.89/69.89 [170]~P1(x1702)+~P1(x1701)+P1(f32(x1701,x1702)) % 69.89/69.89 [171]~P4(x1712)+~P4(x1711)+P4(f49(x1711,x1712)) % 69.89/69.89 [172]~P4(x1722)+~P4(x1721)+P4(f47(x1721,x1722)) % 69.89/69.89 [176]~P1(x1762)+~E(f32(a52,x1762),x1761)+P5(x1761,f48(a52)) % 69.89/69.89 [178]~P1(x1782)+~E(f32(a54,x1782),x1781)+P5(x1781,f48(a54)) % 69.89/69.89 [203]~P1(x2031)+~P5(x2032,a53)+P5(f32(x2031,x2032),a53) % 69.89/69.89 [222]~P5(x2221,a53)+~P5(x2222,a53)+P5(f31(x2221,x2222),a53) % 69.89/69.89 [196]~P1(x1961)+~P8(x1961,a52)+~P8(x1961,a54)+P8(x1961,a55) % 69.89/69.89 [197]~P1(x1971)+~P8(x1971,a52)+~P2(x1971,a54)+P8(x1971,a55) % 69.89/69.89 [165]~P3(x1651)+P4(x1651)+P5(f4(x1651),x1651)+P1(f3(x1651)) % 69.89/69.89 [192]~P1(x1921)+~P8(x1921,a52)+~P8(x1921,a54)+P1(f18(x1921)) % 69.89/69.89 [193]~P1(x1931)+~P8(x1931,a52)+~P2(x1931,a54)+P1(f18(x1931)) % 69.89/69.89 [208]~P1(x2081)+~P8(x2081,a52)+~P8(x2081,a54)+E(f32(x2081,f18(x2081)),a55) % 69.89/69.89 [209]~P1(x2091)+~P8(x2091,a52)+~P2(x2091,a54)+E(f32(x2091,f18(x2091)),a55) % 69.89/69.89 [253]~P3(x2531)+P4(x2531)+P1(f3(x2531))+~P5(f31(f39(x2531),f4(x2531)),x2531) % 69.89/69.89 [256]~P3(x2561)+P4(x2561)+P5(f4(x2561),x2561)+~P5(f32(f3(x2561),f39(x2561)),x2561) % 69.89/69.89 [268]~P3(x2681)+P4(x2681)+~P5(f31(f39(x2681),f4(x2681)),x2681)+~P5(f32(f3(x2681),f39(x2681)),x2681) % 69.89/69.89 [188]~P1(x1882)+~P1(x1881)+~P8(x1881,x1882)+P2(x1881,x1882) % 69.89/69.89 [228]~P1(x2282)+~P1(x2281)+~P10(x2281,x2282)+P6(a51,x2281,x2282) % 69.89/69.89 [245]~P1(x2452)+~P1(x2451)+P10(x2451,x2452)+~P6(a51,x2451,x2452) % 69.89/69.89 [179]~P1(x1791)+~P1(x1792)+E(x1791,a1)+P1(f5(x1792,x1791)) % 69.89/69.89 [180]~P1(x1801)+~P1(x1802)+E(x1801,a1)+P1(f8(x1802,x1801)) % 69.89/69.89 [198]~P1(x1982)+~P2(x1981,a52)+P1(f18(x1981))+~E(f32(x1981,x1982),a54) % 69.89/69.89 [202]~P1(x2022)+~P2(x2021,a52)+P8(x2021,a55)+~E(f32(x2021,x2022),a54) % 69.89/69.89 [204]~P1(x2042)+~P1(x2041)+~P8(x2041,x2042)+P1(f9(x2041,x2042)) % 69.89/69.89 [213]~P1(x2132)+~P2(x2131,a52)+~E(f32(x2131,x2132),a54)+E(f32(x2131,f18(x2131)),a55) % 69.89/69.89 [221]~P1(x2212)+~P1(x2211)+~P8(x2211,x2212)+E(f32(x2211,f9(x2211,x2212)),x2212) % 69.89/69.89 [258]~P1(x2581)+~P1(x2582)+E(x2581,a1)+E(f31(f32(f5(x2582,x2581),x2581),f8(x2582,x2581)),x2582) % 69.89/69.89 [247]~P1(x2472)+~P6(x2471,x2473,x2472)+P2(x2471,x2472)+~P1(x2473) % 69.89/69.89 [248]~P1(x2482)+~P6(x2481,x2482,x2483)+P2(x2481,x2482)+~P1(x2483) % 69.89/69.89 [163]~P3(x1633)+~P3(x1632)+P3(x1631)+~E(x1631,f49(x1632,x1633)) % 69.89/69.89 [164]~P3(x1643)+~P3(x1642)+P3(x1641)+~E(x1641,f47(x1642,x1643)) % 69.89/69.89 [216]~P1(x2161)+~P4(x2163)+~P5(x2162,x2163)+P5(f32(x2161,x2162),x2163) % 69.89/69.89 [230]P5(x2301,a53)+~E(f31(x2302,x2303),x2301)+~P5(x2303,f48(a54))+~P5(x2302,f48(a52)) % 69.89/69.89 [233]~P4(x2333)+~P5(x2331,x2333)+~P5(x2332,x2333)+P5(f31(x2331,x2332),x2333) % 69.89/69.89 [262]~P1(x2621)+~P5(x2623,x2622)+~E(x2622,f48(x2621))+P1(f12(x2621,x2622,x2623)) % 69.89/69.89 [239]~P1(x2393)+~P1(x2392)+~P1(x2391)+E(f31(f31(x2391,x2392),x2393),f31(x2391,f31(x2392,x2393))) % 69.89/69.89 [240]~P1(x2403)+~P1(x2402)+~P1(x2401)+E(f32(f32(x2401,x2402),x2403),f32(x2401,f32(x2402,x2403))) % 69.89/69.89 [254]~P1(x2543)+~P1(x2542)+~P1(x2541)+E(f31(f32(x2541,x2542),f32(x2541,x2543)),f32(x2541,f31(x2542,x2543))) % 69.89/69.89 [255]~P1(x2552)+~P1(x2553)+~P1(x2551)+E(f31(f32(x2551,x2552),f32(x2553,x2552)),f32(f31(x2551,x2553),x2552)) % 69.89/69.89 [264]~P1(x2641)+~P5(x2643,x2642)+~E(x2642,f48(x2641))+E(f32(x2641,f12(x2641,x2642,x2643)),x2643) % 69.89/69.89 [159]~P1(x1591)+~P1(x1592)+E(x1591,a1)+E(x1592,a1)+~E(f32(x1592,x1591),a1) % 69.89/69.89 [205]~P1(x2052)+~P1(x2051)+~P8(x2051,a54)+P1(f18(x2051))+~E(f32(x2051,x2052),a52) % 69.89/69.89 [206]~P1(x2062)+~P1(x2061)+~P2(x2061,a54)+P1(f18(x2061))+~E(f32(x2061,x2062),a52) % 69.89/69.89 [207]~P1(x2072)+~P1(x2071)+~P8(x2071,a52)+P1(f18(x2071))+~E(f32(x2071,x2072),a54) % 69.89/69.89 [210]~P1(x2102)+~P1(x2101)+~P8(x2101,a54)+P8(x2101,a55)+~E(f32(x2101,x2102),a52) % 69.89/69.89 [211]~P1(x2112)+~P1(x2111)+~P2(x2111,a54)+P8(x2111,a55)+~E(f32(x2111,x2112),a52) % 69.89/69.89 [212]~P1(x2122)+~P1(x2121)+~P8(x2121,a52)+P8(x2121,a55)+~E(f32(x2121,x2122),a54) % 69.89/69.89 [224]~P5(x2241,a53)+~P5(x2242,a53)+E(x2241,a1)+E(x2242,a1)+~P9(f33(x2242),f33(a34)) % 69.89/69.89 [229]~P1(x2292)+~P3(x2291)+P5(f11(x2292,x2291),x2291)+E(x2291,f48(x2292))+P1(f10(x2292,x2291)) % 69.89/69.89 [236]~P3(x2362)+~P3(x2361)+E(x2361,x2362)+P5(f14(x2361,x2362),x2361)+P5(f24(x2361,x2362),x2362) % 69.89/69.89 [250]~P3(x2502)+~P3(x2501)+E(x2501,x2502)+P5(f14(x2501,x2502),x2501)+~P5(f24(x2501,x2502),x2501) % 69.89/69.89 [251]~P3(x2512)+~P3(x2511)+E(x2511,x2512)+P5(f24(x2511,x2512),x2512)+~P5(f14(x2511,x2512),x2512) % 69.89/69.89 [261]~P3(x2612)+~P3(x2611)+E(x2611,x2612)+~P5(f14(x2611,x2612),x2612)+~P5(f24(x2611,x2612),x2611) % 69.89/69.89 [218]~P1(x2182)+~P1(x2181)+~P8(x2181,a54)+~E(f32(x2181,x2182),a52)+E(f32(x2181,f18(x2181)),a55) % 69.89/69.89 [219]~P1(x2192)+~P1(x2191)+~P2(x2191,a54)+~E(f32(x2191,x2192),a52)+E(f32(x2191,f18(x2191)),a55) % 69.89/69.89 [220]~P1(x2202)+~P1(x2201)+~P8(x2201,a52)+~E(f32(x2201,x2202),a54)+E(f32(x2201,f18(x2201)),a55) % 69.89/69.89 [243]~P1(x2431)+~P1(x2432)+E(x2431,a1)+P9(f33(f8(x2432,x2431)),f33(x2431))+E(f8(x2432,x2431),a1) % 69.89/69.89 [246]~P1(x2462)+~P3(x2461)+P5(f11(x2462,x2461),x2461)+E(x2461,f48(x2462))+E(f32(x2462,f10(x2462,x2461)),f11(x2462,x2461)) % 69.89/69.89 [194]~P1(x1942)+~P1(x1941)+~P1(x1943)+P8(x1941,x1942)+~E(f32(x1941,x1943),x1942) % 69.89/69.89 [225]E(x2251,a1)+~E(a34,a1)+~E(f31(x2252,x2253),x2251)+~P5(x2253,f48(a54))+~P5(x2252,f48(a52)) % 69.89/69.89 [227]E(x2271,a1)+~E(f31(x2272,x2273),x2271)+~P5(x2273,f48(a54))+~P5(x2272,f48(a52))+~E(f35(x2271),a1) % 69.89/69.89 [231]E(x2311,a1)+~E(f31(x2312,x2313),x2311)+~P5(x2313,f48(a54))+~P5(x2312,f48(a52))+E(f31(a36,a37),a34) % 69.89/69.89 [232]E(x2321,a1)+P5(a34,a53)+~E(f31(x2322,x2323),x2321)+~P5(x2323,f48(a54))+~P5(x2322,f48(a52)) % 69.89/69.89 [234]E(x2341,a1)+~E(f31(x2342,x2343),x2341)+~P5(x2343,f48(a54))+~P5(x2342,f48(a52))+P5(a36,f48(a52)) % 69.89/69.89 [235]E(x2351,a1)+~E(f31(x2352,x2353),x2351)+~P5(x2353,f48(a54))+~P5(x2352,f48(a52))+P5(a37,f48(a54)) % 69.89/69.89 [238]E(x2381,a1)+~E(f31(x2382,x2383),x2381)+~P5(x2383,f48(a54))+~P5(x2382,f48(a52))+P5(f35(x2381),a53) % 69.89/69.89 [241]E(x2411,a1)+~E(f31(x2412,x2413),x2411)+P5(f40(x2411),f48(a52))+~P5(x2413,f48(a54))+~P5(x2412,f48(a52)) % 69.89/69.89 [242]E(x2421,a1)+~E(f31(x2422,x2423),x2421)+P5(f41(x2421),f48(a54))+~P5(x2423,f48(a54))+~P5(x2422,f48(a52)) % 69.89/69.89 [244]E(x2441,a1)+~E(f31(x2442,x2443),x2441)+~P5(x2443,f48(a54))+~P5(x2442,f48(a52))+E(f31(f40(x2441),f41(x2441)),f35(x2441)) % 69.89/69.89 [249]E(x2491,a1)+~E(f31(x2492,x2493),x2491)+~P5(x2493,f48(a54))+~P5(x2492,f48(a52))+P9(f33(f35(x2491)),f33(x2491)) % 69.89/69.89 [263]~P1(x2632)+~P1(x2631)+~P4(x2633)+P11(x2631,x2632,x2633)+~P5(f31(x2631,f50(x2632)),x2633) % 69.89/69.89 [265]~P1(x2652)+~P1(x2651)+~P4(x2653)+~P11(x2651,x2652,x2653)+P5(f31(x2651,f50(x2652)),x2653) % 69.89/69.89 [199]~P1(x1993)+~P1(x1994)+P5(x1991,x1992)+~E(f32(x1993,x1994),x1991)+~E(x1992,f48(x1993)) % 69.89/69.89 [214]~P3(x2144)+~P3(x2142)+~P5(x2141,x2143)+P5(x2141,x2142)+~E(x2143,f47(x2144,x2142)) % 69.89/69.89 [215]~P3(x2154)+~P3(x2152)+~P5(x2151,x2153)+P5(x2151,x2152)+~E(x2153,f47(x2152,x2154)) % 69.89/69.89 [279]~P3(x2792)+~P3(x2791)+~P5(x2794,x2793)+~E(x2793,f49(x2791,x2792))+P5(f38(x2791,x2792,x2793,x2794),x2791) % 69.89/69.89 [280]~P3(x2802)+~P3(x2801)+~P5(x2804,x2803)+~E(x2803,f49(x2801,x2802))+P5(f43(x2801,x2802,x2803,x2804),x2802) % 69.89/69.90 [287]~P3(x2872)+~P3(x2871)+~P5(x2874,x2873)+~E(x2873,f49(x2871,x2872))+E(f31(f38(x2871,x2872,x2873,x2874),f43(x2871,x2872,x2873,x2874)),x2874) % 69.89/69.90 [217]~P1(x2172)+~P1(x2173)+~P1(x2171)+P1(f18(x2171))+~E(f32(x2171,x2172),a52)+~E(f32(x2171,x2173),a54) % 69.89/69.90 [223]~P1(x2232)+~P1(x2233)+~P1(x2231)+P8(x2231,a55)+~E(f32(x2231,x2232),a52)+~E(f32(x2231,x2233),a54) % 69.89/69.90 [257]~P1(x2573)+~P1(x2572)+~P3(x2571)+~P5(f11(x2572,x2571),x2571)+~E(f11(x2572,x2571),f32(x2572,x2573))+E(x2571,f48(x2572)) % 69.89/69.90 [269]~P1(x2693)+~P1(x2692)+~P2(x2691,x2693)+~P2(x2691,x2692)+P6(x2691,x2692,x2693)+P2(f13(x2692,x2693,x2691),x2693) % 69.89/69.90 [270]~P1(x2703)+~P1(x2702)+~P2(x2701,x2703)+~P2(x2701,x2702)+P6(x2701,x2702,x2703)+P2(f13(x2702,x2703,x2701),x2702) % 69.89/69.90 [271]~P3(x2711)+~P3(x2713)+~P3(x2712)+P5(f42(x2712,x2713,x2711),x2711)+P5(f44(x2712,x2713,x2711),x2712)+E(x2711,f49(x2712,x2713)) % 69.89/69.90 [272]~P3(x2721)+~P3(x2723)+~P3(x2722)+P5(f42(x2722,x2723,x2721),x2721)+P5(f45(x2722,x2723,x2721),x2723)+E(x2721,f49(x2722,x2723)) % 69.89/69.90 [273]~P3(x2731)+~P3(x2733)+~P3(x2732)+P5(f46(x2732,x2733,x2731),x2731)+P5(f46(x2732,x2733,x2731),x2733)+E(x2731,f47(x2732,x2733)) % 69.89/69.90 [274]~P3(x2741)+~P3(x2743)+~P3(x2742)+P5(f46(x2742,x2743,x2741),x2741)+P5(f46(x2742,x2743,x2741),x2742)+E(x2741,f47(x2742,x2743)) % 69.89/69.90 [275]~P1(x2753)+~P1(x2752)+~P2(x2751,x2753)+~P2(x2751,x2752)+P6(x2751,x2752,x2753)+~P8(f13(x2752,x2753,x2751),x2751) % 69.89/69.90 [226]~P1(x2262)+~P1(x2263)+~P1(x2261)+~E(f32(x2261,x2262),a52)+~E(f32(x2261,x2263),a54)+E(f32(x2261,f18(x2261)),a55) % 69.89/69.90 [277]~P3(x2771)+~P3(x2773)+~P3(x2772)+P5(f42(x2772,x2773,x2771),x2771)+E(x2771,f49(x2772,x2773))+E(f31(f44(x2772,x2773,x2771),f45(x2772,x2773,x2771)),f42(x2772,x2773,x2771)) % 69.89/69.90 [266]~P2(x2661,x2663)+~P2(x2661,x2664)+~P6(x2662,x2664,x2663)+P8(x2661,x2662)+~P1(x2663)+~P1(x2664) % 69.89/69.90 [237]~P3(x2374)+~P3(x2373)+~P5(x2371,x2374)+~P5(x2371,x2373)+P5(x2371,x2372)+~E(x2372,f47(x2373,x2374)) % 69.89/69.90 [278]~P1(x2784)+~P1(x2783)+~P4(x2782)+~P4(x2781)+P1(f6(x2781,x2782))+P1(f7(x2781,x2782,x2783,x2784)) % 69.89/69.90 [281]~P1(x2814)+~P1(x2813)+~P4(x2812)+~P4(x2811)+P11(f7(x2811,x2812,x2813,x2814),x2814,x2812)+P1(f6(x2811,x2812)) % 69.89/69.90 [282]~P1(x2824)+~P1(x2823)+~P4(x2822)+~P4(x2821)+P11(f7(x2821,x2822,x2823,x2824),x2823,x2821)+P1(f6(x2821,x2822)) % 69.89/69.90 [284]~P1(x2844)+~P1(x2843)+~P4(x2842)+~P4(x2841)+~P5(f6(x2841,x2842),f49(x2841,x2842))+P1(f7(x2841,x2842,x2843,x2844)) % 69.89/69.90 [285]~P1(x2854)+~P1(x2853)+~P4(x2852)+~P4(x2851)+P11(f7(x2851,x2852,x2853,x2854),x2854,x2852)+~P5(f6(x2851,x2852),f49(x2851,x2852)) % 69.89/69.90 [286]~P1(x2864)+~P1(x2863)+~P4(x2862)+~P4(x2861)+P11(f7(x2861,x2862,x2863,x2864),x2863,x2861)+~P5(f6(x2861,x2862),f49(x2861,x2862)) % 69.89/69.90 [283]~P3(x2831)+~P3(x2833)+~P3(x2832)+~P5(f46(x2832,x2833,x2831),x2831)+~P5(f46(x2832,x2833,x2831),x2833)+~P5(f46(x2832,x2833,x2831),x2832)+E(x2831,f47(x2832,x2833)) % 69.89/69.90 [259]~P5(x2591,a53)+E(x2591,a1)+~E(f31(x2593,x2594),x2592)+E(x2592,a1)+~P5(x2594,f48(a54))+~P5(x2593,f48(a52))+~P9(f33(x2592),f33(a34)) % 69.89/69.90 [252]~P3(x2524)+~P3(x2523)+~P5(x2526,x2524)+~P5(x2525,x2523)+P5(x2521,x2522)+~E(x2522,f49(x2523,x2524))+~E(f31(x2525,x2526),x2521) % 69.89/69.90 [276]~P3(x2761)+~P3(x2763)+~P3(x2762)+~P5(x2765,x2763)+~P5(x2764,x2762)+~P5(f42(x2762,x2763,x2761),x2761)+E(x2761,f49(x2762,x2763))+~E(f31(x2764,x2765),f42(x2762,x2763,x2761)) % 69.89/69.90 [267]E(x2671,a1)+~E(f31(x2673,x2674),x2671)+E(x2672,a1)+~E(f31(x2675,x2676),x2672)+~P5(x2674,f48(a54))+~P5(x2673,f48(a52))+~P5(x2676,f48(a54))+~P5(x2675,f48(a52))+~P9(f33(x2672),f33(a34)) % 69.89/69.90 %EqnAxiom % 69.89/69.90 [1]E(x11,x11) % 69.89/69.90 [2]E(x22,x21)+~E(x21,x22) % 69.89/69.90 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 69.89/69.90 [4]~E(x41,x42)+E(f31(x41,x43),f31(x42,x43)) % 69.89/69.90 [5]~E(x51,x52)+E(f31(x53,x51),f31(x53,x52)) % 69.89/69.90 [6]~E(x61,x62)+E(f32(x61,x63),f32(x62,x63)) % 69.89/69.90 [7]~E(x71,x72)+E(f32(x73,x71),f32(x73,x72)) % 69.89/69.90 [8]~E(x81,x82)+E(f44(x81,x83,x84),f44(x82,x83,x84)) % 69.89/69.90 [9]~E(x91,x92)+E(f44(x93,x91,x94),f44(x93,x92,x94)) % 69.89/69.90 [10]~E(x101,x102)+E(f44(x103,x104,x101),f44(x103,x104,x102)) % 69.89/69.90 [11]~E(x111,x112)+E(f42(x111,x113,x114),f42(x112,x113,x114)) % 69.89/69.90 [12]~E(x121,x122)+E(f42(x123,x121,x124),f42(x123,x122,x124)) % 69.89/69.90 [13]~E(x131,x132)+E(f42(x133,x134,x131),f42(x133,x134,x132)) % 69.89/69.90 [14]~E(x141,x142)+E(f49(x141,x143),f49(x142,x143)) % 69.89/69.90 [15]~E(x151,x152)+E(f49(x153,x151),f49(x153,x152)) % 69.89/69.90 [16]~E(x161,x162)+E(f13(x161,x163,x164),f13(x162,x163,x164)) % 69.89/69.90 [17]~E(x171,x172)+E(f13(x173,x171,x174),f13(x173,x172,x174)) % 69.89/69.90 [18]~E(x181,x182)+E(f13(x183,x184,x181),f13(x183,x184,x182)) % 69.89/69.90 [19]~E(x191,x192)+E(f33(x191),f33(x192)) % 69.89/69.90 [20]~E(x201,x202)+E(f48(x201),f48(x202)) % 69.89/69.90 [21]~E(x211,x212)+E(f40(x211),f40(x212)) % 69.89/69.90 [22]~E(x221,x222)+E(f7(x221,x223,x224,x225),f7(x222,x223,x224,x225)) % 69.89/69.90 [23]~E(x231,x232)+E(f7(x233,x231,x234,x235),f7(x233,x232,x234,x235)) % 69.89/69.90 [24]~E(x241,x242)+E(f7(x243,x244,x241,x245),f7(x243,x244,x242,x245)) % 69.89/69.90 [25]~E(x251,x252)+E(f7(x253,x254,x255,x251),f7(x253,x254,x255,x252)) % 69.89/69.90 [26]~E(x261,x262)+E(f38(x261,x263,x264,x265),f38(x262,x263,x264,x265)) % 69.89/69.90 [27]~E(x271,x272)+E(f38(x273,x271,x274,x275),f38(x273,x272,x274,x275)) % 69.89/69.90 [28]~E(x281,x282)+E(f38(x283,x284,x281,x285),f38(x283,x284,x282,x285)) % 69.89/69.90 [29]~E(x291,x292)+E(f38(x293,x294,x295,x291),f38(x293,x294,x295,x292)) % 69.89/69.90 [30]~E(x301,x302)+E(f41(x301),f41(x302)) % 69.89/69.90 [31]~E(x311,x312)+E(f43(x311,x313,x314,x315),f43(x312,x313,x314,x315)) % 69.89/69.90 [32]~E(x321,x322)+E(f43(x323,x321,x324,x325),f43(x323,x322,x324,x325)) % 69.89/69.90 [33]~E(x331,x332)+E(f43(x333,x334,x331,x335),f43(x333,x334,x332,x335)) % 69.89/69.90 [34]~E(x341,x342)+E(f43(x343,x344,x345,x341),f43(x343,x344,x345,x342)) % 69.89/69.90 [35]~E(x351,x352)+E(f14(x351,x353),f14(x352,x353)) % 69.89/69.90 [36]~E(x361,x362)+E(f14(x363,x361),f14(x363,x362)) % 69.89/69.90 [37]~E(x371,x372)+E(f35(x371),f35(x372)) % 69.89/69.90 [38]~E(x381,x382)+E(f18(x381),f18(x382)) % 69.89/69.90 [39]~E(x391,x392)+E(f47(x391,x393),f47(x392,x393)) % 69.89/69.90 [40]~E(x401,x402)+E(f47(x403,x401),f47(x403,x402)) % 69.89/69.90 [41]~E(x411,x412)+E(f24(x411,x413),f24(x412,x413)) % 69.89/69.90 [42]~E(x421,x422)+E(f24(x423,x421),f24(x423,x422)) % 69.89/69.90 [43]~E(x431,x432)+E(f11(x431,x433),f11(x432,x433)) % 69.89/69.90 [44]~E(x441,x442)+E(f11(x443,x441),f11(x443,x442)) % 69.89/69.90 [45]~E(x451,x452)+E(f50(x451),f50(x452)) % 69.89/69.90 [46]~E(x461,x462)+E(f29(x461),f29(x462)) % 69.89/69.90 [47]~E(x471,x472)+E(f8(x471,x473),f8(x472,x473)) % 69.89/69.90 [48]~E(x481,x482)+E(f8(x483,x481),f8(x483,x482)) % 69.89/69.90 [49]~E(x491,x492)+E(f39(x491),f39(x492)) % 69.89/69.90 [50]~E(x501,x502)+E(f3(x501),f3(x502)) % 69.89/69.90 [51]~E(x511,x512)+E(f6(x511,x513),f6(x512,x513)) % 69.89/69.90 [52]~E(x521,x522)+E(f6(x523,x521),f6(x523,x522)) % 69.89/69.90 [53]~E(x531,x532)+E(f46(x531,x533,x534),f46(x532,x533,x534)) % 69.89/69.90 [54]~E(x541,x542)+E(f46(x543,x541,x544),f46(x543,x542,x544)) % 69.89/69.90 [55]~E(x551,x552)+E(f46(x553,x554,x551),f46(x553,x554,x552)) % 69.89/69.90 [56]~E(x561,x562)+E(f4(x561),f4(x562)) % 69.89/69.90 [57]~E(x571,x572)+E(f9(x571,x573),f9(x572,x573)) % 69.89/69.90 [58]~E(x581,x582)+E(f9(x583,x581),f9(x583,x582)) % 69.89/69.90 [59]~E(x591,x592)+E(f28(x591),f28(x592)) % 69.89/69.90 [60]~E(x601,x602)+E(f45(x601,x603,x604),f45(x602,x603,x604)) % 69.89/69.90 [61]~E(x611,x612)+E(f45(x613,x611,x614),f45(x613,x612,x614)) % 69.89/69.90 [62]~E(x621,x622)+E(f45(x623,x624,x621),f45(x623,x624,x622)) % 69.89/69.90 [63]~E(x631,x632)+E(f19(x631),f19(x632)) % 69.89/69.90 [64]~E(x641,x642)+E(f20(x641),f20(x642)) % 69.89/69.90 [65]~E(x651,x652)+E(f10(x651,x653),f10(x652,x653)) % 69.89/69.90 [66]~E(x661,x662)+E(f10(x663,x661),f10(x663,x662)) % 69.89/69.90 [67]~E(x671,x672)+E(f17(x671),f17(x672)) % 69.89/69.90 [68]~E(x681,x682)+E(f21(x681),f21(x682)) % 69.89/69.90 [69]~E(x691,x692)+E(f12(x691,x693,x694),f12(x692,x693,x694)) % 69.89/69.90 [70]~E(x701,x702)+E(f12(x703,x701,x704),f12(x703,x702,x704)) % 69.89/69.90 [71]~E(x711,x712)+E(f12(x713,x714,x711),f12(x713,x714,x712)) % 69.89/69.90 [72]~E(x721,x722)+E(f5(x721,x723),f5(x722,x723)) % 69.89/69.90 [73]~E(x731,x732)+E(f5(x733,x731),f5(x733,x732)) % 69.89/69.90 [74]~P1(x741)+P1(x742)+~E(x741,x742) % 69.89/69.90 [75]P5(x752,x753)+~E(x751,x752)+~P5(x751,x753) % 69.89/69.90 [76]P5(x763,x762)+~E(x761,x762)+~P5(x763,x761) % 69.89/69.90 [77]~P3(x771)+P3(x772)+~E(x771,x772) % 69.89/69.90 [78]P6(x782,x783,x784)+~E(x781,x782)+~P6(x781,x783,x784) % 69.89/69.90 [79]P6(x793,x792,x794)+~E(x791,x792)+~P6(x793,x791,x794) % 69.89/69.90 [80]P6(x803,x804,x802)+~E(x801,x802)+~P6(x803,x804,x801) % 69.89/69.90 [81]P9(x812,x813)+~E(x811,x812)+~P9(x811,x813) % 69.89/69.90 [82]P9(x823,x822)+~E(x821,x822)+~P9(x823,x821) % 69.89/69.90 [83]~P4(x831)+P4(x832)+~E(x831,x832) % 69.89/69.90 [84]P2(x842,x843)+~E(x841,x842)+~P2(x841,x843) % 69.89/69.90 [85]P2(x853,x852)+~E(x851,x852)+~P2(x853,x851) % 69.89/69.90 [86]P11(x862,x863,x864)+~E(x861,x862)+~P11(x861,x863,x864) % 69.89/69.90 [87]P11(x873,x872,x874)+~E(x871,x872)+~P11(x873,x871,x874) % 69.89/69.90 [88]P11(x883,x884,x882)+~E(x881,x882)+~P11(x883,x884,x881) % 69.89/69.90 [89]P8(x892,x893)+~E(x891,x892)+~P8(x891,x893) % 69.89/69.90 [90]P8(x903,x902)+~E(x901,x902)+~P8(x903,x901) % 69.89/69.90 [91]P10(x912,x913)+~E(x911,x912)+~P10(x911,x913) % 69.89/69.90 [92]P10(x923,x922)+~E(x921,x922)+~P10(x923,x921) % 69.89/69.90 [93]~P7(x931)+P7(x932)+~E(x931,x932) % 69.89/69.90 % 69.89/69.90 %------------------------------------------- % 69.89/69.90 cnf(288,plain, % 69.89/69.90 (~P1(x2881)+P3(f48(x2881))), % 69.89/69.90 inference(equality_inference,[],[137])). % 69.89/69.90 cnf(289,plain, % 69.89/69.90 (~P3(x2891)+~P3(x2892)+P3(f49(x2892,x2891))), % 69.89/69.90 inference(equality_inference,[],[163])). % 69.89/69.90 cnf(290,plain, % 69.89/69.90 (~P3(x2901)+~P3(x2902)+P3(f47(x2902,x2901))), % 69.89/69.90 inference(equality_inference,[],[164])). % 69.89/69.90 cnf(291,plain, % 69.89/69.90 (~P1(x2911)+P5(f32(a52,x2911),f48(a52))), % 69.89/69.90 inference(equality_inference,[],[176])). % 69.89/69.90 cnf(292,plain, % 69.89/69.90 (~P1(x2921)+P5(f32(a54,x2921),f48(a54))), % 69.89/69.90 inference(equality_inference,[],[178])). % 69.89/69.90 cnf(293,plain, % 69.89/69.90 (P8(x2931,f32(x2931,x2932))+~P1(f32(x2931,x2932))+~P1(x2931)+~P1(x2932)), % 69.89/69.90 inference(equality_inference,[],[194])). % 69.89/69.90 cnf(296,plain, % 69.89/69.90 (P5(f31(x2961,x2962),a53)+~P5(x2962,f48(a54))+~P5(x2961,f48(a52))), % 69.89/69.90 inference(equality_inference,[],[230])). % 69.89/69.90 cnf(301,plain, % 69.89/69.90 (~P5(x3011,x3012)+~P3(x3013)+~P5(x3011,x3013)+~P3(x3012)+P5(x3011,f47(x3012,x3013))), % 69.89/69.90 inference(equality_inference,[],[237])). % 69.89/69.90 cnf(308,plain, % 69.89/69.90 (~P1(x3081)+~P5(x3082,f48(x3081))+P1(f12(x3081,f48(x3081),x3082))), % 69.89/69.90 inference(equality_inference,[],[262])). % 69.89/69.90 cnf(309,plain, % 69.89/69.90 (~P1(x3091)+~P5(x3092,f48(x3091))+E(f32(x3091,f12(x3091,f48(x3091),x3092)),x3092)), % 69.89/69.90 inference(equality_inference,[],[264])). % 69.89/69.90 cnf(313,plain, % 69.89/69.90 (E(a27,f31(a26,a30))), % 69.89/69.90 inference(scs_inference,[],[108,2])). % 69.89/69.90 cnf(314,plain, % 69.89/69.90 (~E(a1,f31(a26,a30))), % 69.89/69.90 inference(scs_inference,[],[129,108,2,3])). % 69.89/69.90 cnf(315,plain, % 69.89/69.90 (P5(f31(a26,a30),f49(f48(a52),f48(a54)))), % 69.89/69.90 inference(scs_inference,[],[129,108,127,2,3,75])). % 69.89/69.90 cnf(316,plain, % 69.89/69.90 (P5(a27,a53)), % 69.89/69.90 inference(scs_inference,[],[129,108,127,125,2,3,75,76])). % 69.89/69.90 cnf(321,plain, % 69.89/69.90 (P8(a52,a1)), % 69.89/69.90 inference(scs_inference,[],[94,96,99,102,116,117,129,108,109,127,125,2,3,75,76,190,188,194])). % 69.89/69.90 cnf(323,plain, % 69.89/69.90 (P5(a27,f47(a53,a53))), % 69.89/69.90 inference(scs_inference,[],[94,96,99,102,106,116,117,129,108,109,127,125,2,3,75,76,190,188,194,301])). % 69.89/69.90 cnf(325,plain, % 69.89/69.90 (~P1(f31(a26,a30))+P1(a27)), % 69.89/69.90 inference(scs_inference,[],[94,96,99,102,106,116,117,129,108,109,127,125,2,3,75,76,190,188,194,301,74])). % 69.89/69.90 cnf(326,plain, % 69.89/69.90 (~P5(f31(a26,a30),a53)+P1(a27)), % 69.89/69.90 inference(scs_inference,[],[94,96,99,102,106,116,117,129,108,109,127,125,2,3,75,76,190,188,194,301,74,151])). % 69.89/69.90 cnf(336,plain, % 69.89/69.90 (E(a52,f32(a55,a2))), % 69.89/69.90 inference(scs_inference,[],[113,2])). % 69.89/69.90 cnf(338,plain, % 69.89/69.90 (P8(f32(a55,a2),a1)), % 69.89/69.90 inference(scs_inference,[],[321,113,117,2,85,89])). % 69.89/69.90 cnf(340,plain, % 69.89/69.90 (P5(f31(a26,a30),a53)), % 69.89/69.90 inference(scs_inference,[],[316,313,321,113,115,117,2,85,89,90,75])). % 69.89/69.90 cnf(341,plain, % 69.89/69.90 (P6(a55,f32(a55,a2),a54)), % 69.89/69.90 inference(scs_inference,[],[316,313,321,113,115,117,126,2,85,89,90,75,79])). % 69.89/69.90 cnf(342,plain, % 69.89/69.90 (P1(f32(a55,a2))), % 69.89/69.90 inference(scs_inference,[],[316,313,321,113,115,117,96,126,2,85,89,90,75,79,74])). % 69.89/69.90 cnf(347,plain, % 69.89/69.90 (P8(a52,a52)), % 69.89/69.90 inference(scs_inference,[],[94,316,313,321,113,115,106,103,110,117,96,126,2,85,89,90,75,79,74,188,301,194])). % 69.89/69.90 cnf(350,plain, % 69.89/69.90 (P2(f32(a55,a2),a1)), % 69.89/69.90 inference(scs_inference,[],[94,316,313,321,113,115,106,103,110,117,96,126,2,85,89,90,75,79,74,188,301,194,83,84])). % 69.89/69.90 cnf(354,plain, % 69.89/69.90 (E(x3541,a54)+~E(x3541,f32(a55,a15))), % 69.89/69.90 inference(scs_inference,[],[94,316,313,321,113,115,114,106,103,110,117,96,126,2,85,89,90,75,79,74,188,301,194,83,84,93,78,76,3])). % 69.89/69.90 cnf(359,plain, % 69.89/69.90 (P1(a27)), % 69.89/69.90 inference(scs_inference,[],[340,326])). % 69.89/69.90 cnf(360,plain, % 69.89/69.90 (E(a54,f32(a55,a15))), % 69.89/69.90 inference(scs_inference,[],[114,2])). % 69.89/69.90 cnf(361,plain, % 69.89/69.90 (P8(f32(a55,a2),a52)), % 69.89/69.90 inference(scs_inference,[],[336,347,114,2,89])). % 69.89/69.90 cnf(362,plain, % 69.89/69.90 (P8(a52,f32(a55,a2))), % 69.89/69.90 inference(scs_inference,[],[336,347,114,2,89,90])). % 69.89/69.90 cnf(363,plain, % 69.89/69.90 (P2(a55,f32(a55,a15))), % 69.89/69.90 inference(scs_inference,[],[336,347,114,118,2,89,90,85])). % 69.89/69.90 cnf(364,plain, % 69.89/69.90 (P6(a55,f32(a55,a2),f32(a55,a15))), % 69.89/69.90 inference(scs_inference,[],[336,341,347,114,118,2,89,90,85,80])). % 69.89/69.90 cnf(365,plain, % 69.89/69.90 (P5(f32(a55,a2),f48(a52))), % 69.89/69.90 inference(scs_inference,[],[336,341,347,114,118,121,2,89,90,85,80,75])). % 69.89/69.90 cnf(366,plain, % 69.89/69.90 (P1(f32(a55,a15))), % 69.89/69.90 inference(scs_inference,[],[336,341,347,114,118,97,121,2,89,90,85,80,75,74])). % 69.89/69.90 cnf(367,plain, % 69.89/69.90 (P6(a55,a52,f32(a55,a15))), % 69.89/69.90 inference(scs_inference,[],[336,341,347,113,114,118,97,121,2,89,90,85,80,75,74,79])). % 69.89/69.90 cnf(370,plain, % 69.89/69.90 (P8(a54,a1)), % 69.89/69.90 inference(scs_inference,[],[94,336,341,347,113,114,118,97,104,111,121,96,2,89,90,85,80,75,74,79,188,194])). % 69.89/69.90 cnf(374,plain, % 69.89/69.90 (P2(f32(a55,a2),a52)), % 69.89/69.90 inference(scs_inference,[],[94,336,341,347,113,114,118,97,104,111,121,96,2,89,90,85,80,75,74,79,188,194,190,84])). % 69.89/69.90 cnf(382,plain, % 69.89/69.90 (E(a54,f32(a54,a25))), % 69.89/69.90 inference(scs_inference,[],[112,2])). % 69.89/69.90 cnf(383,plain, % 69.89/69.90 (P8(f32(a55,a2),f32(a55,a2))), % 69.89/69.90 inference(scs_inference,[],[361,336,112,2,90])). % 69.89/69.90 cnf(384,plain, % 69.89/69.90 (P8(f32(a55,a15),a1)), % 69.89/69.90 inference(scs_inference,[],[360,361,370,336,112,2,90,89])). % 69.89/69.90 cnf(386,plain, % 69.89/69.90 (P2(a52,f32(a55,a2))), % 69.89/69.90 inference(scs_inference,[],[360,361,374,370,336,113,112,2,90,89,85,84])). % 69.89/69.90 cnf(387,plain, % 69.89/69.90 (E(f32(a55,a15),f32(a54,a25))), % 69.89/69.90 inference(scs_inference,[],[360,361,374,370,336,113,114,112,2,90,89,85,84,3])). % 69.89/69.90 cnf(388,plain, % 69.89/69.90 (P5(f32(a55,a15),f48(a54))), % 69.89/69.90 inference(scs_inference,[],[360,361,374,370,336,113,114,112,122,2,90,89,85,84,3,75])). % 69.89/69.90 cnf(389,plain, % 69.89/69.90 (P1(f31(a26,a30))), % 69.89/69.90 inference(scs_inference,[],[313,360,361,374,359,370,336,113,114,112,122,2,90,89,85,84,3,75,74])). % 69.89/69.90 cnf(390,plain, % 69.89/69.90 (P2(a54,a1)), % 69.89/69.90 inference(scs_inference,[],[94,313,360,361,374,359,370,336,113,114,112,122,97,2,90,89,85,84,3,75,74,188])). % 69.89/69.90 cnf(392,plain, % 69.89/69.90 (P8(a54,a54)), % 69.89/69.90 inference(scs_inference,[],[94,313,360,361,374,359,370,336,113,114,105,112,122,97,2,90,89,85,84,3,75,74,188,194])). % 69.89/69.90 cnf(403,plain, % 69.89/69.90 (P1(a27)), % 69.89/69.90 inference(scs_inference,[],[389,325])). % 69.89/69.90 cnf(404,plain, % 69.89/69.90 (E(f32(a54,a25),f32(a55,a15))), % 69.89/69.90 inference(scs_inference,[],[387,2])). % 69.89/69.90 cnf(405,plain, % 69.89/69.90 (P8(f32(a54,a25),a1)), % 69.89/69.90 inference(scs_inference,[],[387,384,2,89])). % 69.89/69.90 cnf(407,plain, % 69.89/69.90 (P8(a54,f32(a54,a25))), % 69.89/69.90 inference(scs_inference,[],[367,387,382,384,392,2,89,80,90])). % 69.89/69.90 cnf(409,plain, % 69.89/69.90 (P2(f32(a54,a25),a1)), % 69.89/69.90 inference(scs_inference,[],[367,387,363,382,384,392,390,2,89,80,90,85,84])). % 69.89/69.90 cnf(411,plain, % 69.89/69.90 (P5(f32(a54,a25),f48(a54))), % 69.89/69.90 inference(scs_inference,[],[367,387,388,363,382,384,392,336,390,2,89,80,90,85,84,79,75])). % 69.89/69.90 cnf(412,plain, % 69.89/69.90 (P1(f32(a54,a25))), % 69.89/69.90 inference(scs_inference,[],[367,366,387,388,363,382,384,392,336,390,2,89,80,90,85,84,79,75,74])). % 69.89/69.90 cnf(415,plain, % 69.89/69.90 (P8(a55,f32(a54,a25))), % 69.89/69.90 inference(scs_inference,[],[94,367,366,387,388,363,382,384,392,336,101,390,99,2,89,80,90,85,84,79,75,74,188,194])). % 69.89/69.90 cnf(421,plain, % 69.89/69.90 (E(a52,f32(a52,a22))), % 69.89/69.90 inference(scs_inference,[],[110,2])). % 69.89/69.90 cnf(422,plain, % 69.89/69.90 (P8(f32(a54,a25),f32(a54,a25))), % 69.89/69.90 inference(scs_inference,[],[382,407,110,2,89])). % 69.89/69.90 cnf(423,plain, % 69.89/69.90 (P8(a54,f32(a55,a15))), % 69.89/69.90 inference(scs_inference,[],[382,404,407,110,2,89,90])). % 69.89/69.90 cnf(424,plain, % 69.89/69.90 (E(f32(a55,a2),f32(a52,a22))), % 69.89/69.90 inference(scs_inference,[],[382,404,407,113,110,2,89,90,3])). % 69.89/69.90 cnf(425,plain, % 69.89/69.90 (P1(f32(a52,a22))), % 69.89/69.90 inference(scs_inference,[],[382,404,407,113,110,96,2,89,90,3,74])). % 69.89/69.90 cnf(430,plain, % 69.89/69.90 (P2(f32(a55,a2),x4301)+~E(a1,x4301)), % 69.89/69.90 inference(scs_inference,[],[382,350,404,412,407,113,100,110,99,97,96,2,89,90,3,74,188,194,85])). % 69.89/69.90 cnf(431,plain, % 69.89/69.90 (P2(f32(a54,a25),f32(a54,a25))), % 69.89/69.90 inference(scs_inference,[],[382,350,404,412,407,113,100,110,99,97,96,2,89,90,3,74,188,194,85,84])). % 69.89/69.90 cnf(436,plain, % 69.89/69.90 (E(f32(a52,a22),f32(a55,a2))), % 69.89/69.90 inference(scs_inference,[],[424,2])). % 69.89/69.90 cnf(437,plain, % 69.89/69.90 (P8(f32(a55,a2),f32(a52,a22))), % 69.89/69.90 inference(scs_inference,[],[383,424,2,90])). % 69.89/69.90 cnf(440,plain, % 69.89/69.90 (P6(a55,f32(a52,a22),f32(a55,a15))), % 69.89/69.90 inference(scs_inference,[],[364,374,383,424,421,2,90,89,85,79])). % 69.89/69.90 cnf(441,plain, % 69.89/69.90 (P5(f32(a52,a22),f48(a52))), % 69.89/69.90 inference(scs_inference,[],[364,374,365,383,424,421,2,90,89,85,79,75])). % 69.89/69.90 cnf(442,plain, % 69.89/69.90 (P2(f32(a52,a22),a52)), % 69.89/69.90 inference(scs_inference,[],[364,374,365,383,424,421,2,90,89,85,79,75,84])). % 69.89/69.90 cnf(450,plain, % 69.89/69.90 (E(x4501,a1)+~E(x4501,f32(a54,a23))), % 69.89/69.90 inference(scs_inference,[],[364,374,382,387,323,365,383,423,424,421,366,111,97,2,90,89,85,79,75,84,188,80,190,76,93,3])). % 69.89/69.90 cnf(455,plain, % 69.89/69.90 (E(a1,f32(a54,a23))), % 69.89/69.90 inference(scs_inference,[],[111,2])). % 69.89/69.90 cnf(456,plain, % 69.89/69.90 (P8(f32(a55,a15),f32(a54,a25))), % 69.89/69.90 inference(scs_inference,[],[404,422,111,2,89])). % 69.89/69.90 cnf(458,plain, % 69.89/69.90 (P2(f32(a55,a2),f32(a54,a23))), % 69.89/69.90 inference(scs_inference,[],[404,424,350,362,422,111,2,89,90,85])). % 69.89/69.90 cnf(460,plain, % 69.89/69.90 (P5(f32(a54,a23),f48(a52))), % 69.89/69.90 inference(scs_inference,[],[341,404,424,350,362,422,111,119,2,89,90,85,79,75])). % 69.89/69.90 cnf(462,plain, % 69.89/69.90 (P1(f32(a54,a23))), % 69.89/69.90 inference(scs_inference,[],[94,341,404,424,350,362,422,111,119,2,89,90,85,79,75,84,74])). % 69.89/69.90 cnf(474,plain, % 69.89/69.90 (E(a1,f32(a52,a16))), % 69.89/69.90 inference(scs_inference,[],[109,2])). % 69.89/69.90 cnf(476,plain, % 69.89/69.90 (P8(f32(a52,a22),f32(a52,a22))), % 69.89/69.90 inference(scs_inference,[],[404,424,415,437,109,2,90,89])). % 69.89/69.90 cnf(478,plain, % 69.89/69.90 (E(f32(a52,a16),f32(a54,a23))), % 69.89/69.90 inference(scs_inference,[],[404,424,386,415,437,455,109,2,90,89,85,3])). % 69.89/69.90 cnf(479,plain, % 69.89/69.90 (P5(f32(a54,a23),f48(a54))), % 69.89/69.90 inference(scs_inference,[],[404,424,386,415,437,455,109,120,2,90,89,85,3,75])). % 69.89/69.90 cnf(480,plain, % 69.89/69.90 (P1(f32(a52,a16))), % 69.89/69.90 inference(scs_inference,[],[94,404,424,386,415,437,455,109,120,2,90,89,85,3,75,74])). % 69.89/69.90 cnf(484,plain, % 69.89/69.90 (P8(a52,f32(a54,a23))), % 69.89/69.90 inference(scs_inference,[],[94,404,424,421,386,415,437,456,462,455,412,366,109,102,120,96,2,90,89,85,3,75,74,84,188,194])). % 69.89/69.90 cnf(486,plain, % 69.89/69.90 (P2(f32(a55,a2),f32(a52,a16))), % 69.89/69.90 inference(scs_inference,[],[94,404,424,421,386,415,437,456,462,455,412,366,109,102,120,96,2,90,89,85,3,75,74,84,188,194,430])). % 69.89/69.90 cnf(498,plain, % 69.89/69.90 (E(f32(a54,a23),f32(a52,a16))), % 69.89/69.90 inference(scs_inference,[],[478,2])). % 69.89/69.90 cnf(500,plain, % 69.89/69.90 (P8(f32(a55,a2),f32(a52,a16))), % 69.89/69.90 inference(scs_inference,[],[424,478,338,474,2,89,90])). % 69.89/69.90 cnf(503,plain, % 69.89/69.90 (P5(f32(a52,a16),f48(a52))), % 69.89/69.90 inference(scs_inference,[],[424,421,442,458,478,338,474,119,2,89,90,85,84,75])). % 69.89/69.90 cnf(506,plain, % 69.89/69.90 (P8(a54,f32(a52,a16))), % 69.89/69.90 inference(scs_inference,[],[424,421,442,458,478,480,338,474,484,462,104,119,97,96,2,89,90,85,84,75,188,194])). % 69.89/69.90 cnf(517,plain, % 69.89/69.90 (E(a53,f49(f48(a52),f48(a54)))), % 69.89/69.90 inference(scs_inference,[],[125,2])). % 69.89/69.90 cnf(519,plain, % 69.89/69.90 (P8(f32(a52,a22),f32(a52,a16))), % 69.89/69.90 inference(scs_inference,[],[424,478,500,125,2,90,89])). % 69.89/69.90 cnf(520,plain, % 69.89/69.90 (P2(f32(a54,a25),f32(a52,a16))), % 69.89/69.90 inference(scs_inference,[],[424,474,478,409,500,125,2,90,89,85])). % 69.89/69.90 cnf(521,plain, % 69.89/69.90 (P4(f49(f48(a52),f48(a54)))), % 69.89/69.90 inference(scs_inference,[],[424,474,478,409,500,107,125,2,90,89,85,83])). % 69.89/69.90 cnf(523,plain, % 69.89/69.90 (P3(f49(f48(a52),f48(a54)))), % 69.89/69.90 inference(scs_inference,[],[424,474,478,409,486,500,106,107,125,2,90,89,85,83,84,77])). % 69.89/69.90 cnf(524,plain, % 69.89/69.90 (P5(f32(a52,a16),f48(a54))), % 69.89/69.90 inference(scs_inference,[],[424,474,478,409,486,498,479,500,106,107,125,2,90,89,85,83,84,77,75])). % 69.89/69.90 cnf(525,plain, % 69.89/69.90 (P2(a54,f32(a52,a16))), % 69.89/69.90 inference(scs_inference,[],[424,474,478,409,486,498,479,500,506,480,106,107,125,97,2,90,89,85,83,84,77,75,188])). % 69.89/69.90 cnf(527,plain, % 69.89/69.90 (P5(f31(a26,a30),f47(a53,f49(f48(a52),f48(a54))))), % 69.89/69.90 inference(scs_inference,[],[315,340,424,474,478,409,486,498,479,500,506,480,106,107,125,97,2,90,89,85,83,84,77,75,188,301])). % 69.89/69.90 cnf(533,plain, % 69.89/69.90 (P8(a1,f32(a1,a1))+~P1(f32(a1,a1))), % 69.89/69.90 inference(scs_inference,[],[94,315,340,421,424,440,474,478,409,411,486,498,479,500,506,480,106,107,125,97,2,90,89,85,83,84,77,75,188,301,78,93,76,74,293])). % 69.89/69.90 cnf(544,plain, % 69.89/69.90 (P2(a54,a54)), % 69.89/69.90 inference(scs_inference,[],[404,424,478,361,527,431,519,520,392,108,97,89,90,85,84,75,188])). % 69.89/69.90 cnf(556,plain, % 69.89/69.90 (P8(f32(a54,a25),f32(a52,a16))), % 69.89/69.90 inference(scs_inference,[],[474,405,90])). % 69.89/69.90 cnf(557,plain, % 69.89/69.90 (P8(f32(a54,a25),f32(a55,a15))), % 69.89/69.90 inference(scs_inference,[],[382,474,405,423,90,89])). % 69.89/69.90 cnf(569,plain, % 69.89/69.90 (P8(f32(a54,a25),a54)), % 69.89/69.90 inference(scs_inference,[],[382,478,392,520,85,89])). % 69.89/69.90 cnf(571,plain, % 69.89/69.90 (P2(f32(a54,a25),a54)), % 69.89/69.90 inference(scs_inference,[],[382,478,498,484,392,520,544,85,89,90,84])). % 69.89/69.90 cnf(587,plain, % 69.89/69.90 (P2(f32(a55,a15),a54)), % 69.89/69.90 inference(scs_inference,[],[404,478,506,556,571,525,90,85,89,84])). % 69.89/69.90 cnf(593,plain, % 69.89/69.90 (P8(f32(a55,a15),f32(a55,a15))), % 69.89/69.90 inference(scs_inference,[],[404,557,89])). % 69.89/69.90 cnf(605,plain, % 69.89/69.90 (P8(f32(a55,a15),a54)), % 69.89/69.90 inference(scs_inference,[],[404,569,89])). % 69.89/69.90 cnf(709,plain, % 69.89/69.90 (P4(f48(f19(f32(a55,a15))))), % 69.89/69.90 inference(scs_inference,[],[388,133,156])). % 69.89/69.90 cnf(822,plain, % 69.89/69.90 (P5(x8221,a53)+~E(f31(f32(a55,a2),a1),x8221)), % 69.89/69.90 inference(scs_inference,[],[365,120,230])). % 69.89/69.90 cnf(831,plain, % 69.89/69.90 (P5(f31(f32(a55,a2),a1),a53)), % 69.89/69.90 inference(equality_inference,[],[822])). % 69.89/69.90 cnf(840,plain, % 69.89/69.90 (P3(f49(f48(a1),f48(a1)))), % 69.89/69.90 inference(scs_inference,[],[94,288,289])). % 69.89/69.90 cnf(929,plain, % 69.89/69.90 (P5(f32(a54,a25),x9291)+~E(x9291,f48(a55))), % 69.89/69.90 inference(scs_inference,[],[387,101,99,199])). % 69.89/69.90 cnf(934,plain, % 69.89/69.90 (P5(f32(a54,a25),f48(a55))), % 69.89/69.90 inference(equality_inference,[],[929])). % 69.89/69.90 cnf(935,plain, % 69.89/69.90 (P5(f32(a55,a15),f48(a55))), % 69.89/69.90 inference(scs_inference,[],[404,934,75])). % 69.89/69.90 cnf(954,plain, % 69.89/69.90 (P5(a52,x9541)+~E(x9541,f48(a55))), % 69.89/69.90 inference(scs_inference,[],[113,100,99,199])). % 69.89/69.90 cnf(959,plain, % 69.89/69.90 (P5(a52,f48(a55))), % 69.89/69.90 inference(equality_inference,[],[954])). % 69.89/69.90 cnf(964,plain, % 69.89/69.90 (P5(a54,x9641)+~E(x9641,f48(a55))), % 69.89/69.90 inference(scs_inference,[],[114,101,99,199])). % 69.89/69.90 cnf(969,plain, % 69.89/69.90 (P5(a54,f48(a55))), % 69.89/69.90 inference(equality_inference,[],[964])). % 69.89/69.90 cnf(2101,plain, % 69.89/69.90 (E(f32(a1,f50(a23)),a1)), % 69.89/69.90 inference(scs_inference,[],[104,135,132])). % 69.89/69.90 cnf(2102,plain, % 69.89/69.90 (E(a1,f32(a1,f50(a23)))), % 69.89/69.90 inference(scs_inference,[],[2101,2])). % 69.89/69.90 cnf(2103,plain, % 69.89/69.90 (P1(f32(a1,f50(a23)))), % 69.89/69.90 inference(scs_inference,[],[94,2101,2,74])). % 69.89/69.90 cnf(2104,plain, % 69.89/69.90 (E(f32(a54,a23),f32(a1,f50(a23)))), % 69.89/69.90 inference(scs_inference,[],[111,94,2101,2,74,3])). % 69.89/69.90 cnf(2116,plain, % 69.89/69.90 (P5(f32(a1,f50(a23)),x21161)+~E(x21161,f48(a54))), % 69.89/69.90 inference(scs_inference,[],[104,360,424,517,111,94,97,2101,2,74,3,194,430,84,93,89,188,83,77,163,199])). % 69.89/69.90 cnf(2118,plain, % 69.89/69.90 (P5(f32(a1,f50(a23)),f48(a54))), % 69.89/69.90 inference(equality_inference,[],[2116])). % 69.89/69.90 cnf(2173,plain, % 69.89/69.90 (E(f32(a1,f50(a23)),f32(a52,a16))), % 69.89/69.90 inference(scs_inference,[],[478,2104,2103,102,96,3,194,2])). % 69.89/69.90 cnf(2174,plain, % 69.89/69.90 (P8(f32(a52,a22),f32(a1,f50(a23)))), % 69.89/69.90 inference(scs_inference,[],[421,478,2104,2103,102,96,3,194,2,89])). % 69.89/69.90 cnf(2181,plain, % 69.89/69.90 (P5(f32(a1,f50(a23)),x21811)+~E(x21811,f48(a52))), % 69.89/69.90 inference(scs_inference,[],[421,478,517,2104,2103,102,96,3,194,2,89,83,188,93,77,163,199])). % 69.89/69.90 cnf(2183,plain, % 69.89/69.90 (P5(f32(a1,f50(a23)),f48(a52))), % 69.89/69.90 inference(equality_inference,[],[2181])). % 69.89/69.90 cnf(2184,plain, % 69.89/69.90 (P8(f32(a55,a2),f32(a1,f50(a23)))), % 69.89/69.90 inference(scs_inference,[],[436,2174,89])). % 69.89/69.90 cnf(2201,plain, % 69.89/69.90 (E(f32(f17(f32(a55,a2)),a1),a1)), % 69.89/69.90 inference(scs_inference,[],[365,136,155])). % 69.89/69.90 cnf(2202,plain, % 69.89/69.90 (E(a1,f32(f17(f32(a55,a2)),a1))), % 69.89/69.90 inference(scs_inference,[],[2201,2])). % 69.89/69.90 cnf(2204,plain, % 69.89/69.90 (E(f32(a54,a23),f32(f17(f32(a55,a2)),a1))), % 69.89/69.90 inference(scs_inference,[],[111,94,2201,2,74,3])). % 69.89/69.90 cnf(2219,plain, % 69.89/69.90 (E(f32(f17(f32(a55,a2)),a1),f32(a54,a23))), % 69.89/69.90 inference(scs_inference,[],[2204,2])). % 69.89/69.90 cnf(2220,plain, % 69.89/69.90 (E(f32(a52,a16),f32(f17(f32(a55,a2)),a1))), % 69.89/69.90 inference(scs_inference,[],[478,2204,2,3])). % 69.89/69.90 cnf(2234,plain, % 69.89/69.90 (E(f32(f17(f32(a55,a2)),a1),f32(a52,a16))), % 69.89/69.90 inference(scs_inference,[],[2220,2])). % 69.89/69.90 cnf(2661,plain, % 69.89/69.90 (P5(x26611,a53)+~E(f31(f32(a1,f50(a23)),f32(a54,a23)),x26611)), % 69.89/69.90 inference(scs_inference,[],[2183,479,230])). % 69.89/69.90 cnf(2669,plain, % 69.89/69.90 (P5(f31(f32(a1,f50(a23)),f32(a54,a23)),a53)), % 69.89/69.90 inference(equality_inference,[],[2661])). % 69.89/69.90 cnf(2675,plain, % 69.89/69.90 (P5(x26751,a53)+~E(f31(f32(a1,f50(a23)),a30),x26751)), % 69.89/69.90 inference(scs_inference,[],[2183,124,230])). % 69.89/69.90 cnf(2691,plain, % 69.89/69.90 (P5(x26911,a53)+~E(f31(f32(a1,f50(a23)),a1),x26911)), % 69.89/69.90 inference(scs_inference,[],[2183,120,230])). % 69.89/69.90 cnf(2700,plain, % 69.89/69.90 (P5(f31(f32(a1,f50(a23)),a1),a53)), % 69.89/69.90 inference(equality_inference,[],[2691])). % 69.89/69.90 cnf(2907,plain, % 69.89/69.90 (P1(f50(a1))), % 69.89/69.90 inference(scs_inference,[],[94,132])). % 69.89/69.90 cnf(2909,plain, % 69.89/69.90 (P4(f48(a1))), % 69.89/69.90 inference(scs_inference,[],[94,132,133])). % 69.89/69.90 cnf(2911,plain, % 69.89/69.90 (P3(f48(a1))), % 69.89/69.90 inference(scs_inference,[],[94,132,133,288])). % 69.89/69.90 cnf(2913,plain, % 69.89/69.90 (E(f31(a1,a1),a1)), % 69.89/69.90 inference(scs_inference,[],[94,132,133,288,138])). % 69.89/69.90 cnf(2915,plain, % 69.89/69.90 (E(f32(a51,a1),a1)), % 69.89/69.90 inference(scs_inference,[],[94,132,133,288,138,139])). % 69.89/69.90 cnf(2917,plain, % 69.89/69.90 (E(f31(a27,a1),a27)), % 69.89/69.90 inference(scs_inference,[],[94,359,132,133,288,138,139,140])). % 69.89/69.90 cnf(2919,plain, % 69.89/69.90 (E(f32(a1,a51),a1)), % 69.89/69.90 inference(scs_inference,[],[94,359,132,133,288,138,139,140,141])). % 69.89/69.90 cnf(2921,plain, % 69.89/69.90 (E(f32(a1,a1),a1)), % 69.89/69.90 inference(scs_inference,[],[94,359,132,133,288,138,139,140,141,135])). % 69.89/69.90 cnf(2923,plain, % 69.89/69.90 (E(f32(a27,a1),a1)), % 69.89/69.90 inference(scs_inference,[],[94,359,132,133,288,138,139,140,141,135,136])). % 69.89/69.90 cnf(2949,plain, % 69.89/69.90 (E(f31(f50(a1),a1),a1)), % 69.89/69.90 inference(scs_inference,[],[94,460,359,2118,2173,132,133,288,138,139,140,141,135,136,155,156,157,158,19,20,21,30,37,38,45,46,49,50,56,59,63,64,67,68,143])). % 69.89/69.90 cnf(2957,plain, % 69.89/69.90 (P5(f32(a52,a1),f48(a52))), % 69.89/69.90 inference(scs_inference,[],[94,460,359,2669,2118,2173,132,133,288,138,139,140,141,135,136,155,156,157,158,19,20,21,30,37,38,45,46,49,50,56,59,63,64,67,68,143,144,166,167,291])). % 69.89/69.90 cnf(2959,plain, % 69.89/69.90 (P5(f32(a54,a1),f48(a54))), % 69.89/69.90 inference(scs_inference,[],[94,460,359,2669,2118,2173,132,133,288,138,139,140,141,135,136,155,156,157,158,19,20,21,30,37,38,45,46,49,50,56,59,63,64,67,68,143,144,166,167,291,292])). % 69.89/69.90 cnf(2989,plain, % 69.89/69.90 (E(f31(f20(a27),f21(a27)),a27)), % 69.89/69.90 inference(scs_inference,[],[94,460,359,2669,2118,2173,316,132,133,288,138,139,140,141,135,136,155,156,157,158,19,20,21,30,37,38,45,46,49,50,56,59,63,64,67,68,143,144,166,167,291,292,4,5,6,7,14,15,35,36,39,40,41,42,43,44,47,48,51,52,57,58,65,66,72,73,145,146,185])). % 69.89/69.90 cnf(3011,plain, % 69.89/69.90 (E(f32(a52,f28(f32(a54,a23))),f32(a54,a23))), % 69.89/69.90 inference(scs_inference,[],[94,460,359,2669,2118,2173,316,132,133,288,138,139,140,141,135,136,155,156,157,158,19,20,21,30,37,38,45,46,49,50,56,59,63,64,67,68,143,144,166,167,291,292,4,5,6,7,14,15,35,36,39,40,41,42,43,44,47,48,51,52,57,58,65,66,72,73,145,146,185,8,9,10,11,12,13,16,17,18,53,54,55,60,61,62,69,70,71,181,182])). % 69.89/69.90 cnf(3031,plain, % 69.89/69.90 (~E(a51,a1)), % 69.89/69.90 inference(scs_inference,[],[94,128,460,359,2669,2118,2173,524,316,132,133,288,138,139,140,141,135,136,155,156,157,158,19,20,21,30,37,38,45,46,49,50,56,59,63,64,67,68,143,144,166,167,291,292,4,5,6,7,14,15,35,36,39,40,41,42,43,44,47,48,51,52,57,58,65,66,72,73,145,146,185,8,9,10,11,12,13,16,17,18,53,54,55,60,61,62,69,70,71,181,182,183,184,22,23,24,25,26,27,28,29,31,32,33,34,2675,2])). % 69.89/69.90 cnf(3035,plain, % 69.89/69.90 (~P1(x30351)+P3(x30352)+~E(x30352,f48(x30351))), % 69.89/69.90 inference(rename_variables,[],[137])). % 69.89/69.90 cnf(3036,plain, % 69.89/69.90 (P1(f31(a1,a1))), % 69.89/69.90 inference(scs_inference,[],[94,128,709,460,359,2669,2118,2173,524,480,316,132,133,288,138,139,140,141,135,136,155,156,157,158,19,20,21,30,37,38,45,46,49,50,56,59,63,64,67,68,143,144,166,167,291,292,4,5,6,7,14,15,35,36,39,40,41,42,43,44,47,48,51,52,57,58,65,66,72,73,145,146,185,8,9,10,11,12,13,16,17,18,53,54,55,60,61,62,69,70,71,181,182,183,184,22,23,24,25,26,27,28,29,31,32,33,34,2675,2,131,137,169])). % 69.89/69.90 cnf(3038,plain, % 69.89/69.90 (P1(f32(a1,a1))), % 69.89/69.90 inference(scs_inference,[],[94,128,709,460,359,2669,2118,2173,524,480,316,132,133,288,138,139,140,141,135,136,155,156,157,158,19,20,21,30,37,38,45,46,49,50,56,59,63,64,67,68,143,144,166,167,291,292,4,5,6,7,14,15,35,36,39,40,41,42,43,44,47,48,51,52,57,58,65,66,72,73,145,146,185,8,9,10,11,12,13,16,17,18,53,54,55,60,61,62,69,70,71,181,182,183,184,22,23,24,25,26,27,28,29,31,32,33,34,2675,2,131,137,169,170])). % 69.89/69.90 cnf(3050,plain, % 69.89/69.90 (P1(f18(a55))), % 69.89/69.90 inference(scs_inference,[],[94,128,709,460,359,2669,2118,2173,524,95,521,480,840,116,117,316,132,133,288,138,139,140,141,135,136,155,156,157,158,19,20,21,30,37,38,45,46,49,50,56,59,63,64,67,68,143,144,166,167,291,292,4,5,6,7,14,15,35,36,39,40,41,42,43,44,47,48,51,52,57,58,65,66,72,73,145,146,185,8,9,10,11,12,13,16,17,18,53,54,55,60,61,62,69,70,71,181,182,183,184,22,23,24,25,26,27,28,29,31,32,33,34,2675,2,131,137,169,170,171,172,289,290,134,186])). % 69.89/69.90 cnf(3054,plain, % 69.89/69.91 (P5(f32(a52,f32(a52,a16)),f48(a52))), % 69.89/69.91 inference(scs_inference,[],[94,128,709,460,359,2669,2118,2173,524,95,521,480,840,116,2103,117,316,132,133,288,138,139,140,141,135,136,155,156,157,158,19,20,21,30,37,38,45,46,49,50,56,59,63,64,67,68,143,144,166,167,291,292,4,5,6,7,14,15,35,36,39,40,41,42,43,44,47,48,51,52,57,58,65,66,72,73,145,146,185,8,9,10,11,12,13,16,17,18,53,54,55,60,61,62,69,70,71,181,182,183,184,22,23,24,25,26,27,28,29,31,32,33,34,2675,2,131,137,169,170,171,172,289,290,134,186,203,176])). % 69.89/69.91 cnf(3058,plain, % 69.89/69.91 (E(f32(a55,f18(a55)),a55)), % 69.89/69.91 inference(scs_inference,[],[94,128,709,460,359,2669,969,2118,2173,524,95,521,480,840,116,2103,117,316,99,132,133,288,138,139,140,141,135,136,155,156,157,158,19,20,21,30,37,38,45,46,49,50,56,59,63,64,67,68,143,144,166,167,291,292,4,5,6,7,14,15,35,36,39,40,41,42,43,44,47,48,51,52,57,58,65,66,72,73,145,146,185,8,9,10,11,12,13,16,17,18,53,54,55,60,61,62,69,70,71,181,182,183,184,22,23,24,25,26,27,28,29,31,32,33,34,2675,2,131,137,169,170,171,172,289,290,134,186,203,176,308,200])). % 69.89/69.91 cnf(3070,plain, % 69.89/69.91 (~E(f32(f17(f32(a55,a2)),a1),a51)), % 69.89/69.91 inference(scs_inference,[],[94,128,709,2700,460,359,2669,969,2118,2173,831,2202,524,95,521,480,840,116,2103,117,316,99,106,132,133,288,138,139,140,141,135,136,155,156,157,158,19,20,21,30,37,38,45,46,49,50,56,59,63,64,67,68,143,144,166,167,291,292,4,5,6,7,14,15,35,36,39,40,41,42,43,44,47,48,51,52,57,58,65,66,72,73,145,146,185,8,9,10,11,12,13,16,17,18,53,54,55,60,61,62,69,70,71,181,182,183,184,22,23,24,25,26,27,28,29,31,32,33,34,2675,2,131,137,169,170,171,172,289,290,134,186,203,176,308,200,309,222,296,77,74,151,3])). % 69.89/69.91 cnf(3073,plain, % 69.89/69.91 (P1(f5(a1,a51))), % 69.89/69.91 inference(scs_inference,[],[94,128,709,2184,2700,460,359,2669,969,2118,2173,831,2202,524,95,521,480,840,116,2103,117,316,342,99,106,132,133,288,138,139,140,141,135,136,155,156,157,158,19,20,21,30,37,38,45,46,49,50,56,59,63,64,67,68,143,144,166,167,291,292,4,5,6,7,14,15,35,36,39,40,41,42,43,44,47,48,51,52,57,58,65,66,72,73,145,146,185,8,9,10,11,12,13,16,17,18,53,54,55,60,61,62,69,70,71,181,182,183,184,22,23,24,25,26,27,28,29,31,32,33,34,2675,2,131,137,169,170,171,172,289,290,134,186,203,176,308,200,309,222,296,77,74,151,3,204,179])). % 69.89/69.91 cnf(3089,plain, % 69.89/69.91 (P5(f31(f32(a54,a23),f32(a52,a16)),a53)), % 69.89/69.91 inference(scs_inference,[],[94,128,709,2184,2700,605,460,359,2669,969,2118,2173,831,2202,524,95,521,480,840,366,116,2103,117,316,342,99,106,97,132,133,288,138,139,140,141,135,136,155,156,157,158,19,20,21,30,37,38,45,46,49,50,56,59,63,64,67,68,143,144,166,167,291,292,4,5,6,7,14,15,35,36,39,40,41,42,43,44,47,48,51,52,57,58,65,66,72,73,145,146,185,8,9,10,11,12,13,16,17,18,53,54,55,60,61,62,69,70,71,181,182,183,184,22,23,24,25,26,27,28,29,31,32,33,34,2675,2,131,137,169,170,171,172,289,290,134,186,203,176,308,200,309,222,296,77,74,151,3,204,179,180,221,239,240,258,254,255,230])). % 69.89/69.91 cnf(3091,plain, % 69.89/69.91 (~E(f32(a51,a51),a1)), % 69.89/69.91 inference(scs_inference,[],[94,128,709,2184,2700,605,460,359,2669,969,2118,2173,831,2202,524,95,521,480,840,366,116,2103,117,316,342,99,106,97,132,133,288,138,139,140,141,135,136,155,156,157,158,19,20,21,30,37,38,45,46,49,50,56,59,63,64,67,68,143,144,166,167,291,292,4,5,6,7,14,15,35,36,39,40,41,42,43,44,47,48,51,52,57,58,65,66,72,73,145,146,185,8,9,10,11,12,13,16,17,18,53,54,55,60,61,62,69,70,71,181,182,183,184,22,23,24,25,26,27,28,29,31,32,33,34,2675,2,131,137,169,170,171,172,289,290,134,186,203,176,308,200,309,222,296,77,74,151,3,204,179,180,221,239,240,258,254,255,230,159])). % 69.89/69.91 cnf(3096,plain, % 69.89/69.91 (~E(x30961,f48(a1))+P3(x30961)), % 69.89/69.91 inference(scs_inference,[],[94,128,709,2184,2700,605,460,359,2669,969,2118,2173,831,2202,524,95,521,480,840,366,116,2103,117,316,342,99,106,97,132,133,288,138,139,140,141,135,136,155,156,157,158,19,20,21,30,37,38,45,46,49,50,56,59,63,64,67,68,143,144,166,167,291,292,4,5,6,7,14,15,35,36,39,40,41,42,43,44,47,48,51,52,57,58,65,66,72,73,145,146,185,8,9,10,11,12,13,16,17,18,53,54,55,60,61,62,69,70,71,181,182,183,184,22,23,24,25,26,27,28,29,31,32,33,34,2675,2,131,137,169,170,171,172,289,290,134,186,203,176,308,200,309,222,296,77,74,151,3,204,179,180,221,239,240,258,254,255,230,159,301,450,3035])). % 69.89/69.91 cnf(3113,plain, % 69.89/69.91 (P8(a1,f32(a1,a1))), % 69.89/69.91 inference(scs_inference,[],[3038,533])). % 69.89/69.91 cnf(3117,plain, % 69.89/69.91 (P4(f48(f32(a1,a1)))), % 69.89/69.91 inference(scs_inference,[],[3038,291,133])). % 69.89/69.91 cnf(3129,plain, % 69.89/69.91 (P5(f32(a54,f32(a1,a1)),f48(a54))), % 69.89/69.91 inference(scs_inference,[],[3038,2957,2959,291,133,141,157,184,144,132,292])). % 69.89/69.91 cnf(3174,plain, % 69.89/69.91 (E(f31(f32(a1,a1),x31741),f31(a1,x31741))), % 69.89/69.91 inference(scs_inference,[],[3038,2921,2957,2959,3089,3011,291,133,141,157,184,144,132,292,145,140,46,138,57,40,13,24,72,143,135,39,53,181,28,29,146,167,450,156,15,60,9,139,183,38,64,17,8,158,71,4])). % 69.89/69.91 cnf(3179,plain, % 69.89/69.91 (E(f32(f32(a1,a1),x31791),f32(a1,x31791))), % 69.89/69.91 inference(scs_inference,[],[3038,2921,2957,2959,3089,3011,291,133,141,157,184,144,132,292,145,140,46,138,57,40,13,24,72,143,135,39,53,181,28,29,146,167,450,156,15,60,9,139,183,38,64,17,8,158,71,4,166,32,73,6])). % 69.89/69.91 cnf(3223,plain, % 69.89/69.91 (E(f32(x32231,f32(a1,a1)),f32(x32231,a1))), % 69.89/69.91 inference(scs_inference,[],[3038,2921,2957,2959,3089,3011,291,133,141,157,184,144,132,292,145,140,46,138,57,40,13,24,72,143,135,39,53,181,28,29,146,167,450,156,15,60,9,139,183,38,64,17,8,158,71,4,166,32,73,6,48,18,288,59,51,34,20,27,182,136,56,33,155,14,12,67,70,23,36,44,5,21,37,52,19,45,35,11,50,26,68,10,42,49,58,54,69,43,25,7])). % 69.89/69.91 cnf(3237,plain, % 69.89/69.91 (~E(f35(f31(a26,a30)),a1)), % 69.89/69.91 inference(scs_inference,[],[314,3038,2921,2957,2959,3089,3011,340,291,133,141,157,184,144,132,292,145,140,46,138,57,40,13,24,72,143,135,39,53,181,28,29,146,167,450,156,15,60,9,139,183,38,64,17,8,158,71,4,166,32,73,6,48,18,288,59,51,34,20,27,182,136,56,33,155,14,12,67,70,23,36,44,5,21,37,52,19,45,35,11,50,26,68,10,42,49,58,54,69,43,25,7,47,61,22,16,30,63,31,62,55,66,41,65,2,147])). % 69.89/69.91 cnf(3239,plain, % 69.89/69.91 (P5(f35(f31(a26,a30)),a53)), % 69.89/69.91 inference(scs_inference,[],[314,3038,2921,2957,2959,3089,3011,340,291,133,141,157,184,144,132,292,145,140,46,138,57,40,13,24,72,143,135,39,53,181,28,29,146,167,450,156,15,60,9,139,183,38,64,17,8,158,71,4,166,32,73,6,48,18,288,59,51,34,20,27,182,136,56,33,155,14,12,67,70,23,36,44,5,21,37,52,19,45,35,11,50,26,68,10,42,49,58,54,69,43,25,7,47,61,22,16,30,63,31,62,55,66,41,65,2,147,160])). % 69.89/69.91 cnf(3241,plain, % 69.89/69.91 (P5(a36,f48(a52))), % 69.89/69.91 inference(scs_inference,[],[314,3038,2921,2957,2959,3089,3011,340,291,133,141,157,184,144,132,292,145,140,46,138,57,40,13,24,72,143,135,39,53,181,28,29,146,167,450,156,15,60,9,139,183,38,64,17,8,158,71,4,166,32,73,6,48,18,288,59,51,34,20,27,182,136,56,33,155,14,12,67,70,23,36,44,5,21,37,52,19,45,35,11,50,26,68,10,42,49,58,54,69,43,25,7,47,61,22,16,30,63,31,62,55,66,41,65,2,147,160,153])). % 69.89/69.91 cnf(3243,plain, % 69.89/69.91 (P5(a37,f48(a54))), % 69.89/69.91 inference(scs_inference,[],[314,3038,2921,2957,2959,3089,3011,340,291,133,141,157,184,144,132,292,145,140,46,138,57,40,13,24,72,143,135,39,53,181,28,29,146,167,450,156,15,60,9,139,183,38,64,17,8,158,71,4,166,32,73,6,48,18,288,59,51,34,20,27,182,136,56,33,155,14,12,67,70,23,36,44,5,21,37,52,19,45,35,11,50,26,68,10,42,49,58,54,69,43,25,7,47,61,22,16,30,63,31,62,55,66,41,65,2,147,160,153,154])). % 69.89/69.91 cnf(3245,plain, % 69.89/69.91 (P5(f40(f31(a26,a30)),f48(a52))), % 69.89/69.91 inference(scs_inference,[],[314,3038,2921,2957,2959,3089,3011,340,291,133,141,157,184,144,132,292,145,140,46,138,57,40,13,24,72,143,135,39,53,181,28,29,146,167,450,156,15,60,9,139,183,38,64,17,8,158,71,4,166,32,73,6,48,18,288,59,51,34,20,27,182,136,56,33,155,14,12,67,70,23,36,44,5,21,37,52,19,45,35,11,50,26,68,10,42,49,58,54,69,43,25,7,47,61,22,16,30,63,31,62,55,66,41,65,2,147,160,153,154,173])). % 69.89/69.91 cnf(3247,plain, % 69.89/69.91 (P5(f41(f31(a26,a30)),f48(a54))), % 69.89/69.91 inference(scs_inference,[],[314,3038,2921,2957,2959,3089,3011,340,291,133,141,157,184,144,132,292,145,140,46,138,57,40,13,24,72,143,135,39,53,181,28,29,146,167,450,156,15,60,9,139,183,38,64,17,8,158,71,4,166,32,73,6,48,18,288,59,51,34,20,27,182,136,56,33,155,14,12,67,70,23,36,44,5,21,37,52,19,45,35,11,50,26,68,10,42,49,58,54,69,43,25,7,47,61,22,16,30,63,31,62,55,66,41,65,2,147,160,153,154,173,174])). % 69.89/69.91 cnf(3249,plain, % 69.89/69.91 (E(f31(a36,a37),a34)), % 69.89/69.91 inference(scs_inference,[],[314,3038,2921,2957,2959,3089,3011,340,291,133,141,157,184,144,132,292,145,140,46,138,57,40,13,24,72,143,135,39,53,181,28,29,146,167,450,156,15,60,9,139,183,38,64,17,8,158,71,4,166,32,73,6,48,18,288,59,51,34,20,27,182,136,56,33,155,14,12,67,70,23,36,44,5,21,37,52,19,45,35,11,50,26,68,10,42,49,58,54,69,43,25,7,47,61,22,16,30,63,31,62,55,66,41,65,2,147,160,153,154,173,174,149])). % 69.89/69.91 cnf(3257,plain, % 69.89/69.91 (P1(f31(f32(a1,a1),f32(a1,a1)))), % 69.89/69.91 inference(scs_inference,[],[314,3038,2921,2957,2911,2959,3089,3011,340,96,291,133,141,157,184,144,132,292,145,140,46,138,57,40,13,24,72,143,135,39,53,181,28,29,146,167,450,156,15,60,9,139,183,38,64,17,8,158,71,4,166,32,73,6,48,18,288,59,51,34,20,27,182,136,56,33,155,14,12,67,70,23,36,44,5,21,37,52,19,45,35,11,50,26,68,10,42,49,58,54,69,43,25,7,47,61,22,16,30,63,31,62,55,66,41,65,2,147,160,153,154,173,174,149,309,308,290,169])). % 69.89/69.91 cnf(3261,plain, % 69.89/69.91 (P3(f49(a53,a53))), % 69.89/69.91 inference(scs_inference,[],[314,3038,2921,2957,2911,2959,3089,3011,389,340,106,96,291,133,141,157,184,144,132,292,145,140,46,138,57,40,13,24,72,143,135,39,53,181,28,29,146,167,450,156,15,60,9,139,183,38,64,17,8,158,71,4,166,32,73,6,48,18,288,59,51,34,20,27,182,136,56,33,155,14,12,67,70,23,36,44,5,21,37,52,19,45,35,11,50,26,68,10,42,49,58,54,69,43,25,7,47,61,22,16,30,63,31,62,55,66,41,65,2,147,160,153,154,173,174,149,309,308,290,169,134,289])). % 69.89/69.91 cnf(3263,plain, % 69.89/69.91 (P5(f31(a27,a27),a53)), % 69.89/69.91 inference(scs_inference,[],[314,3038,2921,2957,2911,2959,3089,3011,389,316,340,106,96,291,133,141,157,184,144,132,292,145,140,46,138,57,40,13,24,72,143,135,39,53,181,28,29,146,167,450,156,15,60,9,139,183,38,64,17,8,158,71,4,166,32,73,6,48,18,288,59,51,34,20,27,182,136,56,33,155,14,12,67,70,23,36,44,5,21,37,52,19,45,35,11,50,26,68,10,42,49,58,54,69,43,25,7,47,61,22,16,30,63,31,62,55,66,41,65,2,147,160,153,154,173,174,149,309,308,290,169,134,289,222])). % 69.89/69.91 cnf(3277,plain, % 69.89/69.91 (E(f32(a1,a1),f32(a1,f50(a23)))), % 69.89/69.91 inference(scs_inference,[],[94,314,3038,2921,2957,2909,2911,2959,3089,3011,2102,389,316,340,106,96,291,133,141,157,184,144,132,292,145,140,46,138,57,40,13,24,72,143,135,39,53,181,28,29,146,167,450,156,15,60,9,139,183,38,64,17,8,158,71,4,166,32,73,6,48,18,288,59,51,34,20,27,182,136,56,33,155,14,12,67,70,23,36,44,5,21,37,52,19,45,35,11,50,26,68,10,42,49,58,54,69,43,25,7,47,61,22,16,30,63,31,62,55,66,41,65,2,147,160,153,154,173,174,149,309,308,290,169,134,289,222,172,171,170,203,296,151,3])). % 69.89/69.91 cnf(3284,plain, % 69.89/69.91 (P5(f31(f31(a26,a30),f31(a26,a30)),f49(f48(a52),f48(a54)))), % 69.89/69.91 inference(scs_inference,[],[94,3031,314,3038,2921,2957,2909,2911,2959,3089,3011,403,2102,521,95,389,315,316,340,106,96,291,133,141,157,184,144,132,292,145,140,46,138,57,40,13,24,72,143,135,39,53,181,28,29,146,167,450,156,15,60,9,139,183,38,64,17,8,158,71,4,166,32,73,6,48,18,288,59,51,34,20,27,182,136,56,33,155,14,12,67,70,23,36,44,5,21,37,52,19,45,35,11,50,26,68,10,42,49,58,54,69,43,25,7,47,61,22,16,30,63,31,62,55,66,41,65,2,147,160,153,154,173,174,149,309,308,290,169,134,289,222,172,171,170,203,296,151,3,254,240,258,233])). % 69.89/69.91 cnf(3290,plain, % 69.89/69.91 (P1(f8(a51,a51))), % 69.89/69.91 inference(scs_inference,[],[94,3031,314,3038,2921,2957,2909,2911,2959,3089,3011,476,403,425,2102,521,95,389,315,316,340,106,96,291,133,141,157,184,144,132,292,145,140,46,138,57,40,13,24,72,143,135,39,53,181,28,29,146,167,450,156,15,60,9,139,183,38,64,17,8,158,71,4,166,32,73,6,48,18,288,59,51,34,20,27,182,136,56,33,155,14,12,67,70,23,36,44,5,21,37,52,19,45,35,11,50,26,68,10,42,49,58,54,69,43,25,7,47,61,22,16,30,63,31,62,55,66,41,65,2,147,160,153,154,173,174,149,309,308,290,169,134,289,222,172,171,170,203,296,151,3,254,240,258,233,239,204,180])). % 69.89/69.91 cnf(3292,plain, % 69.89/69.91 (P1(f5(a51,a51))), % 69.89/69.91 inference(scs_inference,[],[94,3031,314,3038,2921,2957,2909,2911,2959,3089,3011,476,403,425,2102,521,95,389,315,316,340,106,96,291,133,141,157,184,144,132,292,145,140,46,138,57,40,13,24,72,143,135,39,53,181,28,29,146,167,450,156,15,60,9,139,183,38,64,17,8,158,71,4,166,32,73,6,48,18,288,59,51,34,20,27,182,136,56,33,155,14,12,67,70,23,36,44,5,21,37,52,19,45,35,11,50,26,68,10,42,49,58,54,69,43,25,7,47,61,22,16,30,63,31,62,55,66,41,65,2,147,160,153,154,173,174,149,309,308,290,169,134,289,222,172,171,170,203,296,151,3,254,240,258,233,239,204,180,179])). % 69.89/69.91 cnf(3298,plain, % 69.89/69.91 (P8(f32(a1,a1),f32(f32(a1,a1),f32(a1,a1)))), % 69.89/69.91 inference(scs_inference,[],[94,3031,314,3038,2921,2957,2909,2911,2959,3089,3011,476,403,425,2102,521,95,389,315,316,340,106,96,291,133,141,157,184,144,132,292,145,140,46,138,57,40,13,24,72,143,135,39,53,181,28,29,146,167,450,156,15,60,9,139,183,38,64,17,8,158,71,4,166,32,73,6,48,18,288,59,51,34,20,27,182,136,56,33,155,14,12,67,70,23,36,44,5,21,37,52,19,45,35,11,50,26,68,10,42,49,58,54,69,43,25,7,47,61,22,16,30,63,31,62,55,66,41,65,2,147,160,153,154,173,174,149,309,308,290,169,134,289,222,172,171,170,203,296,151,3,254,240,258,233,239,204,180,179,221,255,293])). % 69.89/69.91 cnf(3302,plain, % 69.89/69.91 (P5(a1,f48(f32(a1,a1)))), % 69.89/69.91 inference(scs_inference,[],[94,3031,314,3038,2921,2957,2909,2911,2959,3089,3011,476,403,425,2102,521,95,389,315,316,340,106,96,291,133,141,157,184,144,132,292,145,140,46,138,57,40,13,24,72,143,135,39,53,181,28,29,146,167,450,156,15,60,9,139,183,38,64,17,8,158,71,4,166,32,73,6,48,18,288,59,51,34,20,27,182,136,56,33,155,14,12,67,70,23,36,44,5,21,37,52,19,45,35,11,50,26,68,10,42,49,58,54,69,43,25,7,47,61,22,16,30,63,31,62,55,66,41,65,2,147,160,153,154,173,174,149,309,308,290,169,134,289,222,172,171,170,203,296,151,3,254,240,258,233,239,204,180,179,221,255,293,224,199])). % 69.89/69.91 cnf(3304,plain, % 69.89/69.91 (P8(a1,a1)), % 69.89/69.91 inference(scs_inference,[],[94,3031,314,3038,2921,2957,2909,2911,2959,3089,3011,476,403,425,2102,521,95,389,315,316,340,106,96,291,133,141,157,184,144,132,292,145,140,46,138,57,40,13,24,72,143,135,39,53,181,28,29,146,167,450,156,15,60,9,139,183,38,64,17,8,158,71,4,166,32,73,6,48,18,288,59,51,34,20,27,182,136,56,33,155,14,12,67,70,23,36,44,5,21,37,52,19,45,35,11,50,26,68,10,42,49,58,54,69,43,25,7,47,61,22,16,30,63,31,62,55,66,41,65,2,147,160,153,154,173,174,149,309,308,290,169,134,289,222,172,171,170,203,296,151,3,254,240,258,233,239,204,180,179,221,255,293,224,199,194])). % 69.89/69.91 cnf(3361,plain, % 69.89/69.91 (P5(f20(f31(a27,a27)),f48(a52))), % 69.89/69.91 inference(scs_inference,[],[3036,3263,3241,3243,133,291,132,138,157,144,135,136,184,292,141,166])). % 69.89/69.91 cnf(3392,plain, % 69.89/69.91 (P5(f21(f31(a27,a27)),f48(a54))), % 69.89/69.91 inference(scs_inference,[],[3036,2915,3263,3241,3243,133,291,132,138,157,144,135,136,184,292,141,166,146,53,143,158,156,38,181,145,48,13,183,140,182,9,6,14,288,52,24,167])). % 69.89/69.91 cnf(3405,plain, % 69.89/69.91 (E(f48(f32(a51,a1)),f48(a1))), % 69.89/69.91 inference(scs_inference,[],[3036,2915,3263,3241,3243,133,291,132,138,157,144,135,136,184,292,141,166,146,53,143,158,156,38,181,145,48,13,183,140,182,9,6,14,288,52,24,167,40,139,29,17,39,64,11,46,28,44,20])). % 69.89/69.91 cnf(3459,plain, % 69.89/69.91 (~E(a1,f32(a51,a51))), % 69.89/69.91 inference(scs_inference,[],[3036,2915,3091,3263,3241,3243,133,291,132,138,157,144,135,136,184,292,141,166,146,53,143,158,156,38,181,145,48,13,183,140,182,9,6,14,288,52,24,167,40,139,29,17,39,64,11,46,28,44,20,4,12,60,27,36,8,57,68,15,22,73,45,155,32,51,67,72,35,37,7,31,62,54,23,21,71,5,56,70,59,34,58,66,63,61,18,50,65,69,19,41,33,10,49,30,26,25,42,47,16,43,55,2])). % 69.89/69.91 cnf(3462,plain, % 69.89/69.91 (P5(f35(f35(f31(a26,a30))),a53)), % 69.89/69.91 inference(scs_inference,[],[3036,2915,3091,3263,3241,3243,3237,3239,96,133,291,132,138,157,144,135,136,184,292,141,166,146,53,143,158,156,38,181,145,48,13,183,140,182,9,6,14,288,52,24,167,40,139,29,17,39,64,11,46,28,44,20,4,12,60,27,36,8,57,68,15,22,73,45,155,32,51,67,72,35,37,7,31,62,54,23,21,71,5,56,70,59,34,58,66,63,61,18,50,65,69,19,41,33,10,49,30,26,25,42,47,16,43,55,2,308,160])). % 69.89/69.91 cnf(3468,plain, % 69.89/69.91 (P5(f31(f31(a27,a27),f31(a27,a27)),a53)), % 69.89/69.91 inference(scs_inference,[],[3036,2915,3091,3261,3263,3241,3243,3237,3239,96,133,291,132,138,157,144,135,136,184,292,141,166,146,53,143,158,156,38,181,145,48,13,183,140,182,9,6,14,288,52,24,167,40,139,29,17,39,64,11,46,28,44,20,4,12,60,27,36,8,57,68,15,22,73,45,155,32,51,67,72,35,37,7,31,62,54,23,21,71,5,56,70,59,34,58,66,63,61,18,50,65,69,19,41,33,10,49,30,26,25,42,47,16,43,55,2,308,160,309,290,222])). % 69.89/69.91 cnf(3474,plain, % 69.89/69.91 (P4(f49(a53,a53))), % 69.89/69.91 inference(scs_inference,[],[3036,2915,3091,3261,3263,3241,3243,3237,3239,107,96,133,291,132,138,157,144,135,136,184,292,141,166,146,53,143,158,156,38,181,145,48,13,183,140,182,9,6,14,288,52,24,167,40,139,29,17,39,64,11,46,28,44,20,4,12,60,27,36,8,57,68,15,22,73,45,155,32,51,67,72,35,37,7,31,62,54,23,21,71,5,56,70,59,34,58,66,63,61,18,50,65,69,19,41,33,10,49,30,26,25,42,47,16,43,55,2,308,160,309,290,222,174,169,171])). % 69.89/69.91 cnf(3480,plain, % 69.89/69.91 (~E(f35(f35(f31(a26,a30))),a1)), % 69.89/69.91 inference(scs_inference,[],[3036,2915,3091,3261,3263,3241,3243,3237,3239,107,96,133,291,132,138,157,144,135,136,184,292,141,166,146,53,143,158,156,38,181,145,48,13,183,140,182,9,6,14,288,52,24,167,40,139,29,17,39,64,11,46,28,44,20,4,12,60,27,36,8,57,68,15,22,73,45,155,32,51,67,72,35,37,7,31,62,54,23,21,71,5,56,70,59,34,58,66,63,61,18,50,65,69,19,41,33,10,49,30,26,25,42,47,16,43,55,2,308,160,309,290,222,174,169,171,173,289,147])). % 69.89/69.91 cnf(3482,plain, % 69.89/69.91 (P4(f47(a53,a53))), % 69.89/69.91 inference(scs_inference,[],[3036,2915,3091,3261,3263,3241,3243,3237,3239,107,96,133,291,132,138,157,144,135,136,184,292,141,166,146,53,143,158,156,38,181,145,48,13,183,140,182,9,6,14,288,52,24,167,40,139,29,17,39,64,11,46,28,44,20,4,12,60,27,36,8,57,68,15,22,73,45,155,32,51,67,72,35,37,7,31,62,54,23,21,71,5,56,70,59,34,58,66,63,61,18,50,65,69,19,41,33,10,49,30,26,25,42,47,16,43,55,2,308,160,309,290,222,174,169,171,173,289,147,172])). % 69.89/69.91 cnf(3484,plain, % 69.89/69.91 (P5(f32(a1,f31(a27,a27)),a53)), % 69.89/69.91 inference(scs_inference,[],[94,3036,2915,3091,3261,3263,3241,3243,3237,3239,107,96,133,291,132,138,157,144,135,136,184,292,141,166,146,53,143,158,156,38,181,145,48,13,183,140,182,9,6,14,288,52,24,167,40,139,29,17,39,64,11,46,28,44,20,4,12,60,27,36,8,57,68,15,22,73,45,155,32,51,67,72,35,37,7,31,62,54,23,21,71,5,56,70,59,34,58,66,63,61,18,50,65,69,19,41,33,10,49,30,26,25,42,47,16,43,55,2,308,160,309,290,222,174,169,171,173,289,147,172,203])). % 69.89/69.91 cnf(3486,plain, % 69.89/69.91 (P1(f32(f31(a1,a1),f31(a1,a1)))), % 69.89/69.91 inference(scs_inference,[],[94,3036,2915,3091,3261,3263,3241,3243,3237,3239,107,96,133,291,132,138,157,144,135,136,184,292,141,166,146,53,143,158,156,38,181,145,48,13,183,140,182,9,6,14,288,52,24,167,40,139,29,17,39,64,11,46,28,44,20,4,12,60,27,36,8,57,68,15,22,73,45,155,32,51,67,72,35,37,7,31,62,54,23,21,71,5,56,70,59,34,58,66,63,61,18,50,65,69,19,41,33,10,49,30,26,25,42,47,16,43,55,2,308,160,309,290,222,174,169,171,173,289,147,172,203,170])). % 69.89/69.91 cnf(3488,plain, % 69.89/69.91 (P5(f31(a36,a37),a53)), % 69.89/69.91 inference(scs_inference,[],[94,3036,2915,3091,3261,3263,3241,3243,3237,3239,107,96,133,291,132,138,157,144,135,136,184,292,141,166,146,53,143,158,156,38,181,145,48,13,183,140,182,9,6,14,288,52,24,167,40,139,29,17,39,64,11,46,28,44,20,4,12,60,27,36,8,57,68,15,22,73,45,155,32,51,67,72,35,37,7,31,62,54,23,21,71,5,56,70,59,34,58,66,63,61,18,50,65,69,19,41,33,10,49,30,26,25,42,47,16,43,55,2,308,160,309,290,222,174,169,171,173,289,147,172,203,170,296])). % 69.89/69.91 cnf(3490,plain, % 69.89/69.91 (P1(f31(a27,a27))), % 69.89/69.91 inference(scs_inference,[],[94,3036,2915,3091,3261,3263,3241,3243,3237,3239,107,106,96,133,291,132,138,157,144,135,136,184,292,141,166,146,53,143,158,156,38,181,145,48,13,183,140,182,9,6,14,288,52,24,167,40,139,29,17,39,64,11,46,28,44,20,4,12,60,27,36,8,57,68,15,22,73,45,155,32,51,67,72,35,37,7,31,62,54,23,21,71,5,56,70,59,34,58,66,63,61,18,50,65,69,19,41,33,10,49,30,26,25,42,47,16,43,55,2,308,160,309,290,222,174,169,171,173,289,147,172,203,170,296,151])). % 69.89/69.91 cnf(3492,plain, % 69.89/69.91 (~E(f32(a51,a51),f32(a51,a1))), % 69.89/69.91 inference(scs_inference,[],[94,3036,2915,3091,3261,3263,3241,3243,3237,3239,107,106,96,133,291,132,138,157,144,135,136,184,292,141,166,146,53,143,158,156,38,181,145,48,13,183,140,182,9,6,14,288,52,24,167,40,139,29,17,39,64,11,46,28,44,20,4,12,60,27,36,8,57,68,15,22,73,45,155,32,51,67,72,35,37,7,31,62,54,23,21,71,5,56,70,59,34,58,66,63,61,18,50,65,69,19,41,33,10,49,30,26,25,42,47,16,43,55,2,308,160,309,290,222,174,169,171,173,289,147,172,203,170,296,151,3])). % 69.89/69.91 cnf(3493,plain, % 69.89/69.91 (P2(a1,a1)), % 69.89/69.91 inference(scs_inference,[],[94,3304,3036,2915,3091,3261,3263,3241,3243,3237,3239,107,106,96,133,291,132,138,157,144,135,136,184,292,141,166,146,53,143,158,156,38,181,145,48,13,183,140,182,9,6,14,288,52,24,167,40,139,29,17,39,64,11,46,28,44,20,4,12,60,27,36,8,57,68,15,22,73,45,155,32,51,67,72,35,37,7,31,62,54,23,21,71,5,56,70,59,34,58,66,63,61,18,50,65,69,19,41,33,10,49,30,26,25,42,47,16,43,55,2,308,160,309,290,222,174,169,171,173,289,147,172,203,170,296,151,3,188])). % 69.89/69.91 cnf(3499,plain, % 69.89/69.91 (P5(f32(a1,a1),f48(f32(a1,a1)))), % 69.89/69.91 inference(scs_inference,[],[94,3304,3036,2915,3091,3261,3263,3241,3243,3117,3302,3237,3239,107,95,106,96,133,291,132,138,157,144,135,136,184,292,141,166,146,53,143,158,156,38,181,145,48,13,183,140,182,9,6,14,288,52,24,167,40,139,29,17,39,64,11,46,28,44,20,4,12,60,27,36,8,57,68,15,22,73,45,155,32,51,67,72,35,37,7,31,62,54,23,21,71,5,56,70,59,34,58,66,63,61,18,50,65,69,19,41,33,10,49,30,26,25,42,47,16,43,55,2,308,160,309,290,222,174,169,171,173,289,147,172,203,170,296,151,3,188,254,240,216])). % 69.89/69.91 cnf(3503,plain, % 69.89/69.91 (P5(f31(a1,a1),f48(f32(a1,a1)))), % 69.89/69.91 inference(scs_inference,[],[94,3304,3036,2915,3091,3261,3263,3241,3243,3117,3302,3237,3239,107,95,106,96,133,291,132,138,157,144,135,136,184,292,141,166,146,53,143,158,156,38,181,145,48,13,183,140,182,9,6,14,288,52,24,167,40,139,29,17,39,64,11,46,28,44,20,4,12,60,27,36,8,57,68,15,22,73,45,155,32,51,67,72,35,37,7,31,62,54,23,21,71,5,56,70,59,34,58,66,63,61,18,50,65,69,19,41,33,10,49,30,26,25,42,47,16,43,55,2,308,160,309,290,222,174,169,171,173,289,147,172,203,170,296,151,3,188,254,240,216,221,233])). % 69.89/69.91 cnf(3505,plain, % 69.89/69.91 (P1(f9(a1,a1))), % 69.89/69.91 inference(scs_inference,[],[94,3304,3036,2915,3091,3261,3263,3241,3243,3117,3302,3237,3239,107,95,106,96,133,291,132,138,157,144,135,136,184,292,141,166,146,53,143,158,156,38,181,145,48,13,183,140,182,9,6,14,288,52,24,167,40,139,29,17,39,64,11,46,28,44,20,4,12,60,27,36,8,57,68,15,22,73,45,155,32,51,67,72,35,37,7,31,62,54,23,21,71,5,56,70,59,34,58,66,63,61,18,50,65,69,19,41,33,10,49,30,26,25,42,47,16,43,55,2,308,160,309,290,222,174,169,171,173,289,147,172,203,170,296,151,3,188,254,240,216,221,233,204])). % 69.89/69.91 cnf(3511,plain, % 69.89/69.91 (P8(f31(a1,a1),f32(f31(a1,a1),f31(a1,a1)))), % 69.89/69.91 inference(scs_inference,[],[94,3304,3036,2915,3091,3261,3263,3241,3243,3117,3302,3237,3239,107,95,106,96,133,291,132,138,157,144,135,136,184,292,141,166,146,53,143,158,156,38,181,145,48,13,183,140,182,9,6,14,288,52,24,167,40,139,29,17,39,64,11,46,28,44,20,4,12,60,27,36,8,57,68,15,22,73,45,155,32,51,67,72,35,37,7,31,62,54,23,21,71,5,56,70,59,34,58,66,63,61,18,50,65,69,19,41,33,10,49,30,26,25,42,47,16,43,55,2,308,160,309,290,222,174,169,171,173,289,147,172,203,170,296,151,3,188,254,240,216,221,233,204,239,255,293])). % 69.89/69.91 cnf(3513,plain, % 69.89/69.91 (P5(f31(a27,a27),f47(a53,a53))), % 69.89/69.91 inference(scs_inference,[],[94,3304,3036,2915,3091,3261,3263,3241,3243,3117,3302,3237,3239,107,95,106,96,133,291,132,138,157,144,135,136,184,292,141,166,146,53,143,158,156,38,181,145,48,13,183,140,182,9,6,14,288,52,24,167,40,139,29,17,39,64,11,46,28,44,20,4,12,60,27,36,8,57,68,15,22,73,45,155,32,51,67,72,35,37,7,31,62,54,23,21,71,5,56,70,59,34,58,66,63,61,18,50,65,69,19,41,33,10,49,30,26,25,42,47,16,43,55,2,308,160,309,290,222,174,169,171,173,289,147,172,203,170,296,151,3,188,254,240,216,221,233,204,239,255,293,301])). % 69.89/69.91 cnf(3517,plain, % 69.89/69.91 (P3(f47(a53,a53))), % 69.89/69.91 inference(scs_inference,[],[94,3304,3036,2915,3091,3261,3263,3241,3243,3117,3302,3237,3239,107,95,106,96,133,291,132,138,157,144,135,136,184,292,141,166,146,53,143,158,156,38,181,145,48,13,183,140,182,9,6,14,288,52,24,167,40,139,29,17,39,64,11,46,28,44,20,4,12,60,27,36,8,57,68,15,22,73,45,155,32,51,67,72,35,37,7,31,62,54,23,21,71,5,56,70,59,34,58,66,63,61,18,50,65,69,19,41,33,10,49,30,26,25,42,47,16,43,55,2,308,160,309,290,222,174,169,171,173,289,147,172,203,170,296,151,3,188,254,240,216,221,233,204,239,255,293,301,3096,131])). % 69.89/69.91 cnf(3563,plain, % 69.89/69.91 (E(f32(a1,f31(a27,a27)),a1)), % 69.89/69.91 inference(scs_inference,[],[3490,291,133,135])). % 69.89/69.91 cnf(3569,plain, % 69.89/69.91 (P5(f20(f31(a36,a37)),f48(a52))), % 69.89/69.91 inference(scs_inference,[],[3490,3488,291,133,135,144,138,166])). % 69.89/69.91 cnf(3613,plain, % 69.89/69.91 (P5(f21(f31(a36,a37)),f48(a54))), % 69.89/69.91 inference(scs_inference,[],[3490,2919,3488,3392,3361,441,122,291,133,135,144,138,166,132,157,143,136,181,139,158,141,182,184,140,48,146,292,145,183,156,53,288,24,6,38,12,73,4,167])). % 69.89/69.91 cnf(3680,plain, % 69.89/69.91 (P5(f31(f31(a36,a37),f31(a36,a37)),a53)), % 69.89/69.91 inference(scs_inference,[],[3490,3492,2919,3488,3392,3361,441,122,291,133,135,144,138,166,132,157,143,136,181,139,158,141,182,184,140,48,146,292,145,183,156,53,288,24,6,38,12,73,4,167,28,17,51,29,14,64,13,21,52,39,46,68,15,40,31,67,70,20,7,44,8,9,155,22,72,5,58,27,49,11,56,23,37,45,41,35,36,57,54,50,42,62,60,47,32,18,10,59,25,65,71,43,66,61,26,34,19,63,33,55,30,69,16,2,222])). % 69.89/69.91 cnf(3700,plain, % 69.89/69.91 (P1(f31(a36,a37))), % 69.89/69.91 inference(scs_inference,[],[3482,3517,3490,3492,2919,3488,3392,3361,3499,959,441,122,3038,99,106,291,133,135,144,138,166,132,157,143,136,181,139,158,141,182,184,140,48,146,292,145,183,156,53,288,24,6,38,12,73,4,167,28,17,51,29,14,64,13,21,52,39,46,68,15,40,31,67,70,20,7,44,8,9,155,22,72,5,58,27,49,11,56,23,37,45,41,35,36,57,54,50,42,62,60,47,32,18,10,59,25,65,71,43,66,61,26,34,19,63,33,55,30,69,16,2,222,289,308,309,290,169,171,170,296,172,151])). % 69.89/69.91 cnf(3704,plain, % 69.89/69.91 (P2(f32(f17(f32(a55,a2)),a1),a1)), % 69.89/69.91 inference(scs_inference,[],[94,3493,3482,3517,3490,3492,2919,3488,3392,3361,3499,959,441,2202,122,3038,99,106,291,133,135,144,138,166,132,157,143,136,181,139,158,141,182,184,140,48,146,292,145,183,156,53,288,24,6,38,12,73,4,167,28,17,51,29,14,64,13,21,52,39,46,68,15,40,31,67,70,20,7,44,8,9,155,22,72,5,58,27,49,11,56,23,37,45,41,35,36,57,54,50,42,62,60,47,32,18,10,59,25,65,71,43,66,61,26,34,19,63,33,55,30,69,16,2,222,289,308,309,290,169,171,170,296,172,151,203,84])). % 69.89/69.91 cnf(3706,plain, % 69.89/69.91 (P5(f32(a1,f31(a27,a27)),f47(a53,a53))), % 69.89/69.91 inference(scs_inference,[],[94,3493,3482,3517,3513,3490,3492,2919,3488,3392,3361,3499,959,441,2202,122,3038,99,106,291,133,135,144,138,166,132,157,143,136,181,139,158,141,182,184,140,48,146,292,145,183,156,53,288,24,6,38,12,73,4,167,28,17,51,29,14,64,13,21,52,39,46,68,15,40,31,67,70,20,7,44,8,9,155,22,72,5,58,27,49,11,56,23,37,45,41,35,36,57,54,50,42,62,60,47,32,18,10,59,25,65,71,43,66,61,26,34,19,63,33,55,30,69,16,2,222,289,308,309,290,169,171,170,296,172,151,203,84,3,216])). % 69.89/69.91 cnf(3714,plain, % 69.89/69.91 (P5(f31(f31(a27,a27),f31(a27,a27)),f47(a53,a53))), % 69.89/69.91 inference(scs_inference,[],[94,3493,3113,3482,3517,3513,3490,3492,2919,3488,3392,3361,3499,959,441,2202,122,3038,102,99,106,291,133,135,144,138,166,132,157,143,136,181,139,158,141,182,184,140,48,146,292,145,183,156,53,288,24,6,38,12,73,4,167,28,17,51,29,14,64,13,21,52,39,46,68,15,40,31,67,70,20,7,44,8,9,155,22,72,5,58,27,49,11,56,23,37,45,41,35,36,57,54,50,42,62,60,47,32,18,10,59,25,65,71,43,66,61,26,34,19,63,33,55,30,69,16,2,222,289,308,309,290,169,171,170,296,172,151,203,84,3,216,254,221,240,233])). % 69.89/69.91 cnf(3722,plain, % 69.89/69.91 (P5(f32(a1,f50(a23)),f48(f32(a51,a1)))), % 69.89/69.91 inference(scs_inference,[],[94,3493,3113,3482,3517,3513,3490,3492,2919,3488,3392,3361,3405,3499,3277,959,441,2202,122,3038,102,99,106,291,133,135,144,138,166,132,157,143,136,181,139,158,141,182,184,140,48,146,292,145,183,156,53,288,24,6,38,12,73,4,167,28,17,51,29,14,64,13,21,52,39,46,68,15,40,31,67,70,20,7,44,8,9,155,22,72,5,58,27,49,11,56,23,37,45,41,35,36,57,54,50,42,62,60,47,32,18,10,59,25,65,71,43,66,61,26,34,19,63,33,55,30,69,16,2,222,289,308,309,290,169,171,170,296,172,151,203,84,3,216,254,221,240,233,204,239,255,199])). % 69.89/69.91 cnf(3787,plain, % 69.89/69.91 (E(f32(a54,f19(f32(a54,a23))),f32(a54,a23))), % 69.89/69.91 inference(scs_inference,[],[3700,2917,3245,3247,3468,503,479,133,291,138,166,143,135,144,136,181,141,182,146,145,157,132,158,167,140,139,292,48,184,53,288,183])). % 69.89/69.91 cnf(3853,plain, % 69.89/69.91 (E(f33(f31(a27,a1)),f33(a27))), % 69.89/69.91 inference(scs_inference,[],[3700,2917,3245,3247,3468,503,479,133,291,138,166,143,135,144,136,181,141,182,146,145,157,132,158,167,140,139,292,48,184,53,288,183,12,156,28,29,24,46,73,64,15,51,22,21,72,14,17,155,40,52,7,56,27,70,38,44,37,6,13,31,4,8,67,18,42,68,20,47,45,5,39,35,57,36,59,9,61,11,49,60,58,41,50,54,23,62,25,66,71,10,55,30,32,34,19])). % 69.89/69.91 cnf(3884,plain, % 69.89/69.91 (P2(f32(f17(f32(a55,a2)),a1),f32(a54,a23))), % 69.89/69.91 inference(scs_inference,[],[94,3700,2917,3245,3247,3503,3468,3284,3070,3704,3474,935,503,479,455,3038,340,99,523,133,291,138,166,143,135,144,136,181,141,182,146,145,157,132,158,167,140,139,292,48,184,53,288,183,12,156,28,29,24,46,73,64,15,51,22,21,72,14,17,155,40,52,7,56,27,70,38,44,37,6,13,31,4,8,67,18,42,68,20,47,45,5,39,35,57,36,59,9,61,11,49,60,58,41,50,54,23,62,25,66,71,10,55,30,32,34,19,65,16,33,63,43,69,26,2,168,222,308,309,171,296,169,170,172,203,151,85])). % 69.89/69.91 cnf(3885,plain, % 69.89/69.91 (~E(f32(a1,f50(a23)),f32(a51,a51))), % 69.89/69.91 inference(scs_inference,[],[94,3700,3459,2917,3245,3247,3503,3468,3284,3070,3704,3474,935,503,479,2102,455,3038,340,99,523,133,291,138,166,143,135,144,136,181,141,182,146,145,157,132,158,167,140,139,292,48,184,53,288,183,12,156,28,29,24,46,73,64,15,51,22,21,72,14,17,155,40,52,7,56,27,70,38,44,37,6,13,31,4,8,67,18,42,68,20,47,45,5,39,35,57,36,59,9,61,11,49,60,58,41,50,54,23,62,25,66,71,10,55,30,32,34,19,65,16,33,63,43,69,26,2,168,222,308,309,171,296,169,170,172,203,151,85,3])). % 69.89/69.91 cnf(3888,plain, % 69.89/69.91 (P5(f32(a1,f31(f31(a27,a27),f31(a27,a27))),f47(a53,a53))), % 69.89/69.91 inference(scs_inference,[],[94,3700,3459,2917,3714,3245,3247,3503,3468,3284,3070,3704,3474,935,503,3482,479,2102,455,3038,340,100,99,523,133,291,138,166,143,135,144,136,181,141,182,146,145,157,132,158,167,140,139,292,48,184,53,288,183,12,156,28,29,24,46,73,64,15,51,22,21,72,14,17,155,40,52,7,56,27,70,38,44,37,6,13,31,4,8,67,18,42,68,20,47,45,5,39,35,57,36,59,9,61,11,49,60,58,41,50,54,23,62,25,66,71,10,55,30,32,34,19,65,16,33,63,43,69,26,2,168,222,308,309,171,296,169,170,172,203,151,85,3,254,216])). % 69.89/69.91 cnf(3892,plain, % 69.89/69.91 (E(f32(f32(a55,a15),f9(f32(a55,a15),f32(a55,a15))),f32(a55,a15))), % 69.89/69.91 inference(scs_inference,[],[94,3700,3459,2917,3714,3245,3247,3503,3468,3284,3070,3704,3474,593,935,503,3482,479,2102,455,3038,366,340,100,99,523,133,291,138,166,143,135,144,136,181,141,182,146,145,157,132,158,167,140,139,292,48,184,53,288,183,12,156,28,29,24,46,73,64,15,51,22,21,72,14,17,155,40,52,7,56,27,70,38,44,37,6,13,31,4,8,67,18,42,68,20,47,45,5,39,35,57,36,59,9,61,11,49,60,58,41,50,54,23,62,25,66,71,10,55,30,32,34,19,65,16,33,63,43,69,26,2,168,222,308,309,171,296,169,170,172,203,151,85,3,254,216,240,221])). % 69.89/69.91 cnf(3908,plain, % 69.89/69.91 (P2(f32(a52,a16),a1)), % 69.89/69.91 inference(scs_inference,[],[94,3700,3459,2917,3714,3245,3247,3503,3468,3284,3070,3704,3474,587,593,935,503,3117,3482,2234,479,2102,3237,3239,455,3038,366,340,100,99,523,133,291,138,166,143,135,144,136,181,141,182,146,145,157,132,158,167,140,139,292,48,184,53,288,183,12,156,28,29,24,46,73,64,15,51,22,21,72,14,17,155,40,52,7,56,27,70,38,44,37,6,13,31,4,8,67,18,42,68,20,47,45,5,39,35,57,36,59,9,61,11,49,60,58,41,50,54,23,62,25,66,71,10,55,30,32,34,19,65,16,33,63,43,69,26,2,168,222,308,309,171,296,169,170,172,203,151,85,3,254,216,240,221,233,239,255,204,224,450,354,187,84])). % 69.89/69.91 cnf(3991,plain, % 69.89/69.91 (E(f48(f32(a27,a1)),f48(a1))), % 69.89/69.91 inference(scs_inference,[],[3505,3290,2923,3613,3569,3484,3892,3787,121,124,143,135,166,138,181,291,133,141,132,182,157,450,136,144,140,139,145,146,167,288,292,158,48,184,183,29,12,73,354,155,64,24,156,22,52,56,53,72,17,51,27,15,21,67,28,6,18,5,44,46,14,70,20])). % 69.89/69.91 cnf(4036,plain, % 69.89/69.91 (~E(f32(a51,a51),f32(a1,f50(a23)))), % 69.89/69.91 inference(scs_inference,[],[3505,3290,2923,3885,3613,3569,3484,3892,3787,121,124,143,135,166,138,181,291,133,141,132,182,157,450,136,144,140,139,145,146,167,288,292,158,48,184,183,29,12,73,354,155,64,24,156,22,52,56,53,72,17,51,27,15,21,67,28,6,18,5,44,46,14,70,20,13,31,7,38,35,40,8,37,42,23,60,57,4,50,59,61,9,45,47,25,68,32,39,41,36,49,11,58,66,30,62,54,26,19,65,10,43,63,71,33,16,55,69,34,2])). % 69.89/69.91 cnf(4037,plain, % 69.89/69.91 (P8(f32(a52,a16),a1)), % 69.89/69.91 inference(scs_inference,[],[94,3505,3290,3908,2923,3885,3613,3569,3484,3892,3787,121,124,143,135,166,138,181,291,133,141,132,182,157,450,136,144,140,139,145,146,167,288,292,158,48,184,183,29,12,73,354,155,64,24,156,22,52,56,53,72,17,51,27,15,21,67,28,6,18,5,44,46,14,70,20,13,31,7,38,35,40,8,37,42,23,60,57,4,50,59,61,9,45,47,25,68,32,39,41,36,49,11,58,66,30,62,54,26,19,65,10,43,63,71,33,16,55,69,34,2,168])). % 69.89/69.91 cnf(4196,plain, % 69.89/69.91 (~E(a34,a1)), % 69.89/69.91 inference(scs_inference,[],[3292,3054,3129,3058,3680,129,3462,3480,123,120,135,138,143,181,166,133,291,157,141,132,182,288,140,145,158,292,136,146,144,167,139,184,48,12,183,155,22,156,24,51,52,73,6,64,67,18,29,27,354,28,53,17,72,15,21,44,7,46,13,56,38,20,60,8,70,59,4,37,5,45,31,14,42,35,47,57,39,32,9,11,36,23,40,62,26,68,41,61,25,50,43,55,19,30,65,16,58,49,34,66,63,33,10,54,71,69,2,142])). % 69.89/69.91 cnf(4210,plain, % 69.89/69.91 (P5(f40(a27),f48(a52))), % 69.89/69.91 inference(scs_inference,[],[3292,3054,3129,3058,3680,3884,129,3462,3480,359,123,462,120,316,96,135,138,143,181,166,133,291,157,141,132,182,288,140,145,158,292,136,146,144,167,139,184,48,12,183,155,22,156,24,51,52,73,6,64,67,18,29,27,354,28,53,17,72,15,21,44,7,46,13,56,38,20,60,8,70,59,4,37,5,45,31,14,42,35,47,57,39,32,9,11,36,23,40,62,26,68,41,61,25,50,43,55,19,30,65,16,58,49,34,66,63,33,10,54,71,69,2,142,189,195,168,308,160,134,173])). % 69.89/69.91 cnf(4214,plain, % 69.89/69.91 (P5(f41(a27),f48(a54))), % 69.89/69.91 inference(scs_inference,[],[3292,3054,3129,3058,3680,3884,129,3462,3480,359,123,462,120,316,96,135,138,143,181,166,133,291,157,141,132,182,288,140,145,158,292,136,146,144,167,139,184,48,12,183,155,22,156,24,51,52,73,6,64,67,18,29,27,354,28,53,17,72,15,21,44,7,46,13,56,38,20,60,8,70,59,4,37,5,45,31,14,42,35,47,57,39,32,9,11,36,23,40,62,26,68,41,61,25,50,43,55,19,30,65,16,58,49,34,66,63,33,10,54,71,69,2,142,189,195,168,308,160,134,173,147,174])). % 69.89/69.91 cnf(4218,plain, % 69.89/69.91 (P5(f32(a1,f50(a23)),f48(a1))), % 69.89/69.91 inference(scs_inference,[],[3292,3174,3054,3129,3257,3058,3680,3722,3884,129,3405,3462,3480,359,123,462,120,316,96,135,138,143,181,166,133,291,157,141,132,182,288,140,145,158,292,136,146,144,167,139,184,48,12,183,155,22,156,24,51,52,73,6,64,67,18,29,27,354,28,53,17,72,15,21,44,7,46,13,56,38,20,60,8,70,59,4,37,5,45,31,14,42,35,47,57,39,32,9,11,36,23,40,62,26,68,41,61,25,50,43,55,19,30,65,16,58,49,34,66,63,33,10,54,71,69,2,142,189,195,168,308,160,134,173,147,174,74,76])). % 69.89/69.91 cnf(4233,plain, % 69.89/69.91 (P5(f32(a1,f32(a1,f50(a23))),f48(a1))), % 69.89/69.91 inference(scs_inference,[],[94,3292,3174,3179,3054,3129,3257,3058,3680,4036,3722,3888,3884,129,3405,3462,3480,2909,359,441,3517,123,462,120,316,96,135,138,143,181,166,133,291,157,141,132,182,288,140,145,158,292,136,146,144,167,139,184,48,12,183,155,22,156,24,51,52,73,6,64,67,18,29,27,354,28,53,17,72,15,21,44,7,46,13,56,38,20,60,8,70,59,4,37,5,45,31,14,42,35,47,57,39,32,9,11,36,23,40,62,26,68,41,61,25,50,43,55,19,30,65,16,58,49,34,66,63,33,10,54,71,69,2,142,189,195,168,308,160,134,173,147,174,74,76,309,296,169,203,170,151,3,216])). % 69.89/69.91 cnf(4247,plain, % 69.89/69.91 (~P9(f33(a27),f33(a34))), % 69.89/69.91 inference(scs_inference,[],[94,4037,3292,3174,3179,3054,3129,3257,3058,3680,4036,3722,3888,3884,129,3405,3462,3480,2909,359,441,3517,123,462,120,480,316,103,96,135,138,143,181,166,133,291,157,141,132,182,288,140,145,158,292,136,146,144,167,139,184,48,12,183,155,22,156,24,51,52,73,6,64,67,18,29,27,354,28,53,17,72,15,21,44,7,46,13,56,38,20,60,8,70,59,4,37,5,45,31,14,42,35,47,57,39,32,9,11,36,23,40,62,26,68,41,61,25,50,43,55,19,30,65,16,58,49,34,66,63,33,10,54,71,69,2,142,189,195,168,308,160,134,173,147,174,74,76,309,296,169,203,170,151,3,216,254,221,240,239,255,204,224])). % 69.89/69.91 cnf(4260,plain, % 69.89/69.91 (P5(a34,a53)), % 69.89/69.91 inference(scs_inference,[],[94,4037,3292,3174,3179,3054,3129,3853,3991,3257,3058,3680,4036,3722,3888,3884,129,3249,3405,3462,3480,605,2909,359,441,3517,123,3243,462,120,3241,480,316,103,96,135,138,143,181,166,133,291,157,141,132,182,288,140,145,158,292,136,146,144,167,139,184,48,12,183,155,22,156,24,51,52,73,6,64,67,18,29,27,354,28,53,17,72,15,21,44,7,46,13,56,38,20,60,8,70,59,4,37,5,45,31,14,42,35,47,57,39,32,9,11,36,23,40,62,26,68,41,61,25,50,43,55,19,30,65,16,58,49,34,66,63,33,10,54,71,69,2,142,189,195,168,308,160,134,173,147,174,74,76,309,296,169,203,170,151,3,216,254,221,240,239,255,204,224,267,954,964,3096,200,81,150])). % 69.89/69.91 cnf(4396,plain, % 69.89/69.91 (~E(a1,a34)), % 69.89/69.91 inference(scs_inference,[],[4260,4196,2907,3050,4210,4214,2949,138,135,181,185,143,166,133,182,140,141,157,291,167,131,139,288,132,146,145,136,144,158,292,155,184,48,183,156,22,12,27,64,24,53,18,67,15,28,13,52,51,6,20,29,73,60,56,37,21,45,57,17,14,59,44,72,32,9,7,35,47,38,46,23,5,8,36,40,70,4,62,11,61,26,31,39,19,42,43,34,30,65,41,66,49,50,68,25,55,71,58,63,16,33,10,54,69,2])). % 69.89/69.91 cnf(4399,plain, % 69.89/69.91 (P5(f31(a34,a34),a53)), % 69.89/69.91 inference(scs_inference,[],[4260,4196,2907,3050,4210,4214,2949,138,135,181,185,143,166,133,182,140,141,157,291,167,131,139,288,132,146,145,136,144,158,292,155,184,48,183,156,22,12,27,64,24,53,18,67,15,28,13,52,51,6,20,29,73,60,56,37,21,45,57,17,14,59,44,72,32,9,7,35,47,38,46,23,5,8,36,40,70,4,62,11,61,26,31,39,19,42,43,34,30,65,41,66,49,50,68,25,55,71,58,63,16,33,10,54,69,2,189,222])). % 69.89/69.91 cnf(4401,plain, % 69.89/69.91 (P5(f35(a34),a53)), % 69.89/69.91 inference(scs_inference,[],[4260,4196,2907,3050,4210,4214,2949,138,135,181,185,143,166,133,182,140,141,157,291,167,131,139,288,132,146,145,136,144,158,292,155,184,48,183,156,22,12,27,64,24,53,18,67,15,28,13,52,51,6,20,29,73,60,56,37,21,45,57,17,14,59,44,72,32,9,7,35,47,38,46,23,5,8,36,40,70,4,62,11,61,26,31,39,19,42,43,34,30,65,41,66,49,50,68,25,55,71,58,63,16,33,10,54,69,2,189,222,160])). % 69.89/69.91 cnf(4405,plain, % 69.89/69.91 (P9(f33(f35(a34)),f33(a34))), % 69.89/69.91 inference(scs_inference,[],[4260,4196,2907,3050,4210,4214,3298,2949,3223,138,135,181,185,143,166,133,182,140,141,157,291,167,131,139,288,132,146,145,136,144,158,292,155,184,48,183,156,22,12,27,64,24,53,18,67,15,28,13,52,51,6,20,29,73,60,56,37,21,45,57,17,14,59,44,72,32,9,7,35,47,38,46,23,5,8,36,40,70,4,62,11,61,26,31,39,19,42,43,34,30,65,41,66,49,50,68,25,55,71,58,63,16,33,10,54,69,2,189,222,160,90,195])). % 69.89/69.91 cnf(4407,plain, % 69.89/69.91 (~E(f35(a34),a1)), % 69.89/69.91 inference(scs_inference,[],[4260,4196,2907,3050,4210,4214,3298,2949,3223,138,135,181,185,143,166,133,182,140,141,157,291,167,131,139,288,132,146,145,136,144,158,292,155,184,48,183,156,22,12,27,64,24,53,18,67,15,28,13,52,51,6,20,29,73,60,56,37,21,45,57,17,14,59,44,72,32,9,7,35,47,38,46,23,5,8,36,40,70,4,62,11,61,26,31,39,19,42,43,34,30,65,41,66,49,50,68,25,55,71,58,63,16,33,10,54,69,2,189,222,160,90,195,147])). % 69.89/69.91 cnf(4411,plain, % 69.89/69.91 (P8(a1,f32(f31(a1,a1),f31(a1,a1)))), % 69.89/69.91 inference(scs_inference,[],[94,4260,4196,2907,3050,4210,4214,4218,3298,3511,2949,3223,2913,138,135,181,185,143,166,133,182,140,141,157,291,167,131,139,288,132,146,145,136,144,158,292,155,184,48,183,156,22,12,27,64,24,53,18,67,15,28,13,52,51,6,20,29,73,60,56,37,21,45,57,17,14,59,44,72,32,9,7,35,47,38,46,23,5,8,36,40,70,4,62,11,61,26,31,39,19,42,43,34,30,65,41,66,49,50,68,25,55,71,58,63,16,33,10,54,69,2,189,222,160,90,195,147,308,89])). % 69.89/69.91 cnf(4412,plain, % 69.89/69.91 (P5(f41(a34),f48(a54))), % 69.89/69.91 inference(scs_inference,[],[94,4260,4196,2907,3050,4210,4214,4218,3298,3511,2949,3223,2913,138,135,181,185,143,166,133,182,140,141,157,291,167,131,139,288,132,146,145,136,144,158,292,155,184,48,183,156,22,12,27,64,24,53,18,67,15,28,13,52,51,6,20,29,73,60,56,37,21,45,57,17,14,59,44,72,32,9,7,35,47,38,46,23,5,8,36,40,70,4,62,11,61,26,31,39,19,42,43,34,30,65,41,66,49,50,68,25,55,71,58,63,16,33,10,54,69,2,189,222,160,90,195,147,308,89,174])). % 69.89/69.91 cnf(4414,plain, % 69.89/69.91 (P5(f40(a34),f48(a52))), % 69.89/69.91 inference(scs_inference,[],[94,4260,4196,2907,3050,4210,4214,4218,3298,3511,2949,3223,2913,138,135,181,185,143,166,133,182,140,141,157,291,167,131,139,288,132,146,145,136,144,158,292,155,184,48,183,156,22,12,27,64,24,53,18,67,15,28,13,52,51,6,20,29,73,60,56,37,21,45,57,17,14,59,44,72,32,9,7,35,47,38,46,23,5,8,36,40,70,4,62,11,61,26,31,39,19,42,43,34,30,65,41,66,49,50,68,25,55,71,58,63,16,33,10,54,69,2,189,222,160,90,195,147,308,89,174,173])). % 69.89/69.91 cnf(4420,plain, % 69.89/69.91 (P5(f32(a1,a34),a53)), % 69.89/69.91 inference(scs_inference,[],[94,4260,4196,2907,3050,4210,4214,4218,3298,3511,2949,3223,2913,96,138,135,181,185,143,166,133,182,140,141,157,291,167,131,139,288,132,146,145,136,144,158,292,155,184,48,183,156,22,12,27,64,24,53,18,67,15,28,13,52,51,6,20,29,73,60,56,37,21,45,57,17,14,59,44,72,32,9,7,35,47,38,46,23,5,8,36,40,70,4,62,11,61,26,31,39,19,42,43,34,30,65,41,66,49,50,68,25,55,71,58,63,16,33,10,54,69,2,189,222,160,90,195,147,308,89,174,173,309,296,203])). % 69.89/69.91 cnf(4424,plain, % 69.89/69.91 (P1(f32(f50(a1),f50(a1)))), % 69.89/69.91 inference(scs_inference,[],[94,4260,4196,2907,3050,4210,4214,4218,3298,3511,2949,3223,2913,96,138,135,181,185,143,166,133,182,140,141,157,291,167,131,139,288,132,146,145,136,144,158,292,155,184,48,183,156,22,12,27,64,24,53,18,67,15,28,13,52,51,6,20,29,73,60,56,37,21,45,57,17,14,59,44,72,32,9,7,35,47,38,46,23,5,8,36,40,70,4,62,11,61,26,31,39,19,42,43,34,30,65,41,66,49,50,68,25,55,71,58,63,16,33,10,54,69,2,189,222,160,90,195,147,308,89,174,173,309,296,203,169,170])). % 69.89/69.91 cnf(4426,plain, % 69.89/69.91 (P1(a34)), % 69.89/69.91 inference(scs_inference,[],[94,4260,4196,2907,3050,4210,4214,4218,3298,3511,2949,3223,2913,106,96,138,135,181,185,143,166,133,182,140,141,157,291,167,131,139,288,132,146,145,136,144,158,292,155,184,48,183,156,22,12,27,64,24,53,18,67,15,28,13,52,51,6,20,29,73,60,56,37,21,45,57,17,14,59,44,72,32,9,7,35,47,38,46,23,5,8,36,40,70,4,62,11,61,26,31,39,19,42,43,34,30,65,41,66,49,50,68,25,55,71,58,63,16,33,10,54,69,2,189,222,160,90,195,147,308,89,174,173,309,296,203,169,170,151])). % 69.89/69.91 cnf(4428,plain, % 69.89/69.91 (P2(f32(a54,a23),f32(a54,a23))), % 69.89/69.91 inference(scs_inference,[],[94,4260,4196,2907,3050,4210,4214,4218,3298,3511,2949,3223,2913,3884,2219,106,96,138,135,181,185,143,166,133,182,140,141,157,291,167,131,139,288,132,146,145,136,144,158,292,155,184,48,183,156,22,12,27,64,24,53,18,67,15,28,13,52,51,6,20,29,73,60,56,37,21,45,57,17,14,59,44,72,32,9,7,35,47,38,46,23,5,8,36,40,70,4,62,11,61,26,31,39,19,42,43,34,30,65,41,66,49,50,68,25,55,71,58,63,16,33,10,54,69,2,189,222,160,90,195,147,308,89,174,173,309,296,203,169,170,151,84])). % 69.89/69.91 cnf(4659,plain, % 69.89/69.91 ($false), % 69.89/69.91 inference(scs_inference,[],[94,4396,4426,4420,4428,4399,4247,4412,4414,4401,4407,3073,4405,4424,3486,2989,4411,3563,4233,3706,2911,959,462,2202,4196,107,2907,99,96,138,135,143,141,181,291,157,167,166,140,182,133,139,131,145,292,132,288,146,184,158,136,144,155,183,156,48,22,12,67,51,53,6,24,29,15,21,64,27,60,18,45,37,57,59,28,47,73,13,35,52,56,44,20,38,14,7,39,72,26,4,40,62,23,9,17,32,61,36,31,19,42,43,11,46,70,8,5,30,34,65,41,69,16,54,25,58,10,49,68,63,55,33,66,50,71,2,289,81,168,160,222,290,171,147,75,308,173,174,309,172,296,169,203,170,151,3,180,258,179,216,221,240,254,255,204,239,293,224]), % 69.89/69.91 ['proof']). % 69.89/69.91 % SZS output end Proof % 69.89/69.91 % Total time :69.200000s %------------------------------------------------------------------------------