%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : ALG011-1 : TPTP v8.2.0. Released v2.7.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n017.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Jun 24 03:40:36 EDT 2024 % Result : Unsatisfiable 0.55s 0.81s % Output : CNFRefutation 0.55s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.11 % Problem : ALG011-1 : TPTP v8.2.0. Released v2.7.0. % 0.04/0.11 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.10/0.31 % Computer : n017.cluster.edu % 0.10/0.31 % Model : x86_64 x86_64 % 0.10/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.31 % Memory : 8042.1875MB % 0.10/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.31 % CPULimit : 300 % 0.10/0.31 % WCLimit : 300 % 0.10/0.31 % DateTime : Wed Jun 19 15:08:23 EDT 2024 % 0.10/0.32 % CPUTime : % 0.50/0.59 start to proof:theBenchmark % 0.55/0.80 %------------------------------------------- % 0.55/0.80 % File :CSE---1.7 % 0.55/0.80 % Problem :theBenchmark % 0.55/0.80 % Transform :cnf % 0.55/0.80 % Format :tptp:raw % 0.55/0.80 % Command :java -jar mcs_scs.jar %d %s % 0.55/0.80 % 0.55/0.80 % Result :Theorem 0.140000s % 0.55/0.80 % Output :CNFRefutation 0.140000s % 0.55/0.80 %------------------------------------------- % 0.55/0.81 %-------------------------------------------------------------------------- % 0.55/0.81 % File : ALG011-1 : TPTP v8.2.0. Released v2.7.0. % 0.55/0.81 % Domain : General Algebra % 0.55/0.81 % Problem : Partition a monoid into 2 partitions % 0.55/0.81 % Version : [Cla03] axioms. % 0.55/0.81 % English : If C,D is a partition of a monoid M, we cannot have % 0.55/0.81 % C * C subset D and D * D subset C. % 0.55/0.81 % 0.55/0.81 % Refs : [Cla03] Claessen (2003), Email to G. Sutcliffe % 0.55/0.81 % Source : [Cla03] % 0.55/0.81 % Names : % 0.55/0.81 % 0.55/0.81 % Status : Unsatisfiable % 0.55/0.81 % Rating : 0.10 v8.1.0, 0.00 v7.5.0, 0.11 v7.4.0, 0.12 v7.3.0, 0.00 v7.0.0, 0.07 v6.4.0, 0.00 v6.3.0, 0.09 v6.2.0, 0.07 v6.0.0, 0.00 v5.5.0, 0.15 v5.4.0, 0.20 v5.3.0, 0.17 v5.2.0, 0.06 v5.0.0, 0.15 v4.0.1, 0.00 v3.4.0, 0.17 v3.3.0, 0.21 v3.2.0, 0.09 v2.7.0 % 0.55/0.81 % Syntax : Number of clauses : 7 ( 3 unt; 1 nHn; 5 RR) % 0.55/0.81 % Number of literals : 13 ( 1 equ; 6 neg) % 0.55/0.81 % Maximal clause size : 3 ( 1 avg) % 0.55/0.81 % Maximal term depth : 3 ( 1 avg) % 0.55/0.81 % Number of predicates : 3 ( 2 usr; 0 prp; 1-2 aty) % 0.55/0.81 % Number of functors : 3 ( 3 usr; 2 con; 0-2 aty) % 0.55/0.81 % Number of variables : 9 ( 0 sgn) % 0.55/0.81 % SPC : CNF_UNS_RFO_SEQ_NHN % 0.55/0.81 % 0.55/0.81 % Comments : Originally from Thierry Coquand % 0.55/0.81 %-------------------------------------------------------------------------- % 0.55/0.81 cnf(f_is_associative,axiom, % 0.55/0.81 f(X,f(Y,Z)) = f(f(X,Y),Z) ). % 0.55/0.81 % 0.55/0.81 cnf(partitions_union,axiom, % 0.55/0.81 ( c(X) % 0.55/0.81 | d(X) ) ). % 0.55/0.81 % 0.55/0.81 cnf(partitions_exclusive,hypothesis, % 0.55/0.81 ( ~ c(X) % 0.55/0.81 | ~ d(X) ) ). % 0.55/0.81 % 0.55/0.81 cnf(partition_c_not_empty,hypothesis, % 0.55/0.81 c(a1) ). % 0.55/0.81 % 0.55/0.81 cnf(partition_d_not_empty,hypothesis, % 0.55/0.81 d(a2) ). % 0.55/0.81 % 0.55/0.81 cnf(conjecture_1,negated_conjecture, % 0.55/0.81 ( d(f(X,Y)) % 0.55/0.81 | ~ c(X) % 0.55/0.81 | ~ c(Y) ) ). % 0.55/0.81 % 0.55/0.81 cnf(conjecture_2,negated_conjecture, % 0.55/0.81 ( c(f(X,Y)) % 0.55/0.81 | ~ d(X) % 0.55/0.81 | ~ d(Y) ) ). % 0.55/0.81 % 0.55/0.81 %-------------------------------------------------------------------------- % 0.55/0.81 %------------------------------------------- % 0.55/0.81 % Proof found % 0.55/0.81 % SZS status Theorem for theBenchmark % 0.55/0.81 % SZS output start Proof % 0.55/0.81 %ClaNum:14(EqnAxiom:7) % 0.55/0.81 %VarNum:18(SingletonVarNum:9) % 0.55/0.81 %MaxLitNum:3 % 0.55/0.81 %MaxfuncDepth:2 % 0.55/0.81 %SharedTerms:4 % 0.55/0.81 %goalClause: 13 14 % 0.55/0.81 [8]P1(a1) % 0.55/0.81 [9]P2(a2) % 0.55/0.81 [10]E(f3(f3(x101,x102),x103),f3(x101,f3(x102,x103))) % 0.55/0.81 [11]P2(x111)+P1(x111) % 0.55/0.81 [12]~P2(x121)+~P1(x121) % 0.55/0.81 [13]~P2(x132)+~P2(x131)+P1(f3(x131,x132)) % 0.55/0.81 [14]~P1(x142)+~P1(x141)+P2(f3(x141,x142)) % 0.55/0.81 %EqnAxiom % 0.55/0.81 [1]E(x11,x11) % 0.55/0.81 [2]E(x22,x21)+~E(x21,x22) % 0.55/0.81 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.55/0.81 [4]~E(x41,x42)+E(f3(x41,x43),f3(x42,x43)) % 0.55/0.81 [5]~E(x51,x52)+E(f3(x53,x51),f3(x53,x52)) % 0.55/0.81 [6]~P1(x61)+P1(x62)+~E(x61,x62) % 0.55/0.81 [7]~P2(x71)+P2(x72)+~E(x71,x72) % 0.55/0.81 % 0.55/0.81 %------------------------------------------- % 0.55/0.81 cnf(17,plain, % 0.55/0.81 (E(f3(x171,f3(x172,x173)),f3(f3(x171,x172),x173))), % 0.55/0.81 inference(scs_inference,[],[8,10,12,2])). % 0.55/0.81 cnf(18,plain, % 0.55/0.82 (~P2(f3(f3(x181,x182),x183))+P2(f3(x181,f3(x182,x183)))), % 0.55/0.82 inference(scs_inference,[],[8,10,12,2,7])). % 0.55/0.82 cnf(19,plain, % 0.55/0.82 (~P1(f3(x191,x192))+P2(f3(x191,f3(x192,a1)))), % 0.55/0.82 inference(scs_inference,[],[8,10,12,2,7,14])). % 0.55/0.82 cnf(23,plain, % 0.55/0.82 (~P2(f3(x231,f3(x232,x233)))+P2(f3(f3(x231,x232),x233))), % 0.55/0.82 inference(scs_inference,[],[17,7])). % 0.55/0.82 cnf(25,plain, % 0.55/0.82 (~P1(f3(x251,x252))+P2(f3(f3(x251,x252),a1))), % 0.55/0.82 inference(scs_inference,[],[17,7,18,19])). % 0.55/0.82 cnf(29,plain, % 0.55/0.82 (~P1(f3(x291,f3(x292,x293)))+P1(f3(f3(x291,x292),x293))), % 0.55/0.82 inference(scs_inference,[],[17,6])). % 0.55/0.82 cnf(30,plain, % 0.55/0.82 (P2(f3(x301,f3(x302,x303)))+P1(f3(f3(x301,x302),x303))), % 0.55/0.82 inference(scs_inference,[],[17,6,11])). % 0.55/0.82 cnf(32,plain, % 0.55/0.82 (~P2(f3(x321,x322))+P1(f3(f3(a2,x321),x322))), % 0.55/0.82 inference(scs_inference,[],[9,17,6,11,13])). % 0.55/0.82 cnf(37,plain, % 0.55/0.82 (~P2(f3(x371,x372))+P1(f3(a2,f3(x371,x372)))), % 0.55/0.82 inference(scs_inference,[],[10,6,29,32])). % 0.55/0.82 cnf(52,plain, % 0.55/0.82 (P2(f3(f3(a2,a2),a1))), % 0.55/0.82 inference(scs_inference,[],[9,25,13])). % 0.55/0.82 cnf(55,plain, % 0.55/0.82 (P1(f3(a2,f3(a2,f3(a2,a1))))), % 0.55/0.82 inference(scs_inference,[],[52,37,18])). % 0.55/0.82 cnf(58,plain, % 0.55/0.82 (~P2(f3(f3(a2,a2),f3(a2,a1)))), % 0.55/0.82 inference(scs_inference,[],[55,12,18])). % 0.55/0.82 cnf(66,plain, % 0.55/0.82 (~P2(f3(a2,a2))), % 0.55/0.82 inference(scs_inference,[],[9,55,17,12,18,6,19,29,11,13])). % 0.55/0.82 cnf(70,plain, % 0.55/0.82 (P2(f3(a2,f3(a2,a2)))), % 0.55/0.82 inference(scs_inference,[],[9,55,17,12,18,6,19,29,11,13,14,30])). % 0.55/0.82 cnf(81,plain, % 0.55/0.82 (P1(f3(f3(a2,f3(a2,a2)),a2))), % 0.55/0.82 inference(scs_inference,[],[70,23,32])). % 0.55/0.82 cnf(87,plain, % 0.55/0.82 (~P1(f3(a2,a1))+~P1(f3(a2,a2))), % 0.55/0.82 inference(scs_inference,[],[81,58,10,12,6,23,14])). % 0.55/0.82 cnf(91,plain, % 0.55/0.82 (~P1(f3(a2,a1))), % 0.55/0.82 inference(scs_inference,[],[66,87,11])). % 0.55/0.82 cnf(115,plain, % 0.55/0.82 (P1(f3(f3(a2,a2),a1))), % 0.55/0.82 inference(scs_inference,[],[91,11,32])). % 0.55/0.82 cnf(116,plain, % 0.55/0.82 ($false), % 0.55/0.82 inference(scs_inference,[],[115,52,12]), % 0.55/0.82 ['proof']). % 0.55/0.82 % SZS output end Proof % 0.55/0.82 % Total time :0.140000s %------------------------------------------------------------------------------