%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SET012-4 : TPTP v8.2.0. Bugfixed v1.2.1. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n018.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Jun 24 14:20:00 EDT 2024 % Result : Unsatisfiable 63.05s 63.12s % Output : CNFRefutation 63.05s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : SET012-4 : TPTP v8.2.0. Bugfixed v1.2.1. % 0.12/0.13 % Command : java -jar /export/starexec/sandbox2/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 : Sun Jun 23 15:40:54 EDT 2024 % 0.12/0.34 % CPUTime : % 0.20/0.58 start to proof:theBenchmark % 63.05/63.11 %------------------------------------------- % 63.05/63.11 % File :CSE---1.7 % 63.05/63.11 % Problem :theBenchmark % 63.05/63.11 % Transform :cnf % 63.05/63.11 % Format :tptp:raw % 63.05/63.11 % Command :java -jar mcs_scs.jar %d %s % 63.05/63.11 % 63.05/63.11 % Result :Theorem 62.480000s % 63.05/63.11 % Output :CNFRefutation 62.480000s % 63.05/63.11 %------------------------------------------- % 63.05/63.12 %-------------------------------------------------------------------------- % 63.05/63.12 % File : SET012-4 : TPTP v8.2.0. Bugfixed v1.2.1. % 63.05/63.12 % Domain : Set Theory % 63.05/63.12 % Problem : Complement is an involution % 63.05/63.12 % Version : [BL+86] axioms : Reduced > Incomplete. % 63.05/63.12 % English : % 63.05/63.12 % 63.05/63.12 % Refs : [BL+86] Boyer et al. (1986), Set Theory in First-Order Logic: % 63.05/63.12 % Source : [ANL] % 63.05/63.12 % Names : compl.ver2.in [ANL] % 63.05/63.12 % 63.05/63.12 % Status : Unsatisfiable % 63.05/63.12 % Rating : 0.10 v8.1.0, 0.00 v7.5.0, 0.05 v7.4.0, 0.06 v7.3.0, 0.08 v7.1.0, 0.00 v7.0.0, 0.13 v6.4.0, 0.07 v6.3.0, 0.09 v6.2.0, 0.00 v6.1.0, 0.07 v6.0.0, 0.00 v5.5.0, 0.10 v5.4.0, 0.05 v5.3.0, 0.06 v5.2.0, 0.00 v3.3.0, 0.07 v3.2.0, 0.08 v3.1.0, 0.09 v2.7.0, 0.08 v2.6.0, 0.00 v2.5.0, 0.18 v2.4.0, 0.12 v2.2.1, 0.00 v2.1.0, 0.00 v2.0.0 % 63.05/63.12 % Syntax : Number of clauses : 11 ( 4 unt; 3 nHn; 8 RR) % 63.05/63.12 % Number of literals : 21 ( 6 equ; 9 neg) % 63.05/63.12 % Maximal clause size : 3 ( 1 avg) % 63.05/63.12 % Maximal term depth : 2 ( 1 avg) % 63.05/63.12 % Number of predicates : 3 ( 2 usr; 0 prp; 1-2 aty) % 63.05/63.12 % Number of functors : 7 ( 7 usr; 5 con; 0-2 aty) % 63.05/63.12 % Number of variables : 14 ( 2 sgn) % 63.05/63.12 % SPC : CNF_UNS_RFO_SEQ_NHN % 63.05/63.12 % 63.05/63.12 % Comments : % 63.05/63.12 % Bugfixes : v1.2.1 - Missing substitution axioms added. % 63.05/63.12 %-------------------------------------------------------------------------- % 63.05/63.12 %----Axiom A-2, elements of sets are little sets. % 63.05/63.12 cnf(a2,axiom, % 63.05/63.12 ( ~ member(X,Y) % 63.05/63.12 | little_set(X) ) ). % 63.05/63.12 % 63.05/63.12 %----Axiom A-3, principle of extensionality % 63.05/63.12 cnf(extensionality1,axiom, % 63.05/63.12 ( little_set(f1(X,Y)) % 63.05/63.12 | X = Y ) ). % 63.05/63.12 % 63.05/63.12 cnf(extensionality2,axiom, % 63.05/63.12 ( member(f1(X,Y),X) % 63.05/63.12 | member(f1(X,Y),Y) % 63.05/63.12 | X = Y ) ). % 63.05/63.12 % 63.05/63.12 cnf(extensionality3,axiom, % 63.05/63.12 ( ~ member(f1(X,Y),X) % 63.05/63.12 | ~ member(f1(X,Y),Y) % 63.05/63.12 | X = Y ) ). % 63.05/63.12 % 63.05/63.12 %----Axiom B-3, complement % 63.05/63.12 cnf(complement1,axiom, % 63.05/63.12 ( ~ member(Z,complement(X)) % 63.05/63.12 | ~ member(Z,X) ) ). % 63.05/63.12 % 63.05/63.12 cnf(complement2,axiom, % 63.05/63.12 ( member(Z,complement(X)) % 63.05/63.12 | ~ little_set(Z) % 63.05/63.12 | member(Z,X) ) ). % 63.05/63.12 % 63.05/63.12 %----Definition of empty set % 63.05/63.12 cnf(empty_set,axiom, % 63.05/63.12 ~ member(Z,empty_set) ). % 63.05/63.12 % 63.05/63.12 %----Definition of universal set % 63.05/63.12 cnf(universal_set,axiom, % 63.05/63.12 ( member(Z,universal_set) % 63.05/63.12 | ~ little_set(Z) ) ). % 63.05/63.12 % 63.05/63.12 cnf(complement_of_a_is_b,hypothesis, % 63.05/63.12 complement(as) = bs ). % 63.05/63.12 % 63.05/63.12 cnf(complement_of_b_is_c,hypothesis, % 63.05/63.12 complement(bs) = cs ). % 63.05/63.12 % 63.05/63.12 cnf(prove_a_equals_c,negated_conjecture, % 63.05/63.12 as != cs ). % 63.05/63.12 % 63.05/63.12 %-------------------------------------------------------------------------- % 63.05/63.12 %------------------------------------------- % 63.05/63.12 % Proof found % 63.05/63.12 % SZS status Theorem for theBenchmark % 63.05/63.12 % SZS output start Proof % 63.05/63.13 %ClaNum:20(EqnAxiom:9) % 63.05/63.13 %VarNum:35(SingletonVarNum:14) % 63.05/63.13 %MaxLitNum:3 % 63.05/63.13 %MaxfuncDepth:1 % 63.05/63.13 %SharedTerms:10 % 63.05/63.13 %goalClause: 12 % 63.05/63.13 %singleGoalClaCount:1 % 63.05/63.13 [12]~E(a1,a4) % 63.05/63.13 [10]E(f2(a1),a3) % 63.05/63.13 [11]E(f2(a3),a4) % 63.05/63.13 [13]~P1(x131,a5) % 63.05/63.13 [14]~P2(x141)+P1(x141,a6) % 63.05/63.13 [15]P2(x151)+~P1(x151,x152) % 63.05/63.13 [16]E(x161,x162)+P2(f7(x161,x162)) % 63.05/63.13 [18]~P1(x181,x182)+~P1(x181,f2(x182)) % 63.05/63.13 [17]~P2(x171)+P1(x171,x172)+P1(x171,f2(x172)) % 63.05/63.13 [19]E(x191,x192)+P1(f7(x191,x192),x192)+P1(f7(x191,x192),x191) % 63.05/63.13 [20]E(x201,x202)+~P1(f7(x201,x202),x202)+~P1(f7(x201,x202),x201) % 63.05/63.13 %EqnAxiom % 63.05/63.13 [1]E(x11,x11) % 63.05/63.13 [2]E(x22,x21)+~E(x21,x22) % 63.05/63.13 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 63.05/63.13 [4]~E(x41,x42)+E(f2(x41),f2(x42)) % 63.05/63.13 [5]~E(x51,x52)+E(f7(x51,x53),f7(x52,x53)) % 63.05/63.13 [6]~E(x61,x62)+E(f7(x63,x61),f7(x63,x62)) % 63.05/63.13 [7]P1(x72,x73)+~E(x71,x72)+~P1(x71,x73) % 63.05/63.13 [8]P1(x83,x82)+~E(x81,x82)+~P1(x83,x81) % 63.05/63.13 [9]~P2(x91)+P2(x92)+~E(x91,x92) % 63.05/63.13 % 63.05/63.13 %------------------------------------------- % 63.05/63.14 cnf(21,plain, % 63.05/63.14 (E(a3,f2(a1))), % 63.05/63.14 inference(scs_inference,[],[10,2])). % 63.05/63.14 cnf(22,plain, % 63.05/63.14 (~E(a1,f2(a3))), % 63.05/63.14 inference(scs_inference,[],[12,10,11,2,3])). % 63.05/63.14 cnf(26,plain, % 63.05/63.14 (E(a4,f2(a3))), % 63.05/63.14 inference(scs_inference,[],[11,2])). % 63.05/63.14 cnf(37,plain, % 63.05/63.14 (P1(f7(a1,a4),a6)), % 63.05/63.14 inference(scs_inference,[],[12,14,16])). % 63.05/63.14 cnf(38,plain, % 63.05/63.14 (~E(a6,a5)), % 63.05/63.14 inference(scs_inference,[],[13,37,8])). % 63.05/63.14 cnf(91,plain, % 63.05/63.14 (~P1(f7(a4,a1),a1)+~P1(f7(a4,a1),a4)), % 63.05/63.14 inference(scs_inference,[],[12,20,2])). % 63.05/63.14 cnf(105,plain, % 63.05/63.14 (~P2(x1051)+~P1(x1051,f2(a6))), % 63.05/63.14 inference(scs_inference,[],[14,18])). % 63.05/63.14 cnf(519,plain, % 63.05/63.14 (~P1(x5191,f2(a3))+P1(x5191,a4)), % 63.05/63.14 inference(scs_inference,[],[26,2,8])). % 63.05/63.14 cnf(532,plain, % 63.05/63.14 (P2(f7(a4,a1))), % 63.05/63.14 inference(scs_inference,[],[12,2,16])). % 63.05/63.14 cnf(542,plain, % 63.05/63.14 (~E(a4,a1)), % 63.05/63.14 inference(scs_inference,[],[22,11,2,3])). % 63.05/63.14 cnf(1395,plain, % 63.05/63.14 (P2(f7(a5,a6))), % 63.05/63.14 inference(scs_inference,[],[38,16,2])). % 63.05/63.14 cnf(2035,plain, % 63.05/63.14 (P1(f7(a4,a1),a3)+P1(f7(a4,a1),a4)), % 63.05/63.14 inference(scs_inference,[],[532,519,17])). % 63.05/63.14 cnf(3017,plain, % 63.05/63.14 (~P1(x30171,a3)+P1(x30171,f2(a1))), % 63.05/63.14 inference(scs_inference,[],[38,1395,21,13,14,105,2,17,8])). % 63.05/63.14 cnf(3026,plain, % 63.05/63.14 (~P1(x30261,f2(a1))+~P1(x30261,f2(a3))), % 63.05/63.14 inference(scs_inference,[],[10,8,3017,18])). % 63.05/63.14 cnf(3031,plain, % 63.05/63.14 (~P1(x30311,a4)+~P1(x30311,f2(a1))), % 63.05/63.14 inference(scs_inference,[],[26,8,519,3026])). % 63.05/63.14 cnf(3122,plain, % 63.05/63.14 (P1(f7(a4,a1),f2(a3))+P1(f7(a4,a1),a1)), % 63.05/63.14 inference(scs_inference,[],[542,26,19,8])). % 63.05/63.14 cnf(3206,plain, % 63.05/63.14 (P1(f7(a4,a1),f2(a3))+~P1(f7(a4,a1),f2(a1))), % 63.05/63.14 inference(scs_inference,[],[3122,18])). % 63.05/63.14 cnf(3215,plain, % 63.05/63.14 (~P1(f7(a4,a1),f2(a1))+P1(f7(a4,a1),a4)), % 63.05/63.14 inference(scs_inference,[],[3206,519])). % 63.05/63.14 cnf(3218,plain, % 63.05/63.14 (~P1(f7(a4,a1),f2(a1))), % 63.05/63.14 inference(scs_inference,[],[3215,3031])). % 63.05/63.14 cnf(3221,plain, % 63.05/63.14 (~P1(f7(a4,a1),a3)), % 63.05/63.14 inference(scs_inference,[],[3218,3017])). % 63.05/63.14 cnf(3233,plain, % 63.05/63.14 (P1(f7(a4,a1),a4)), % 63.05/63.14 inference(scs_inference,[],[3221,2035])). % 63.05/63.14 cnf(3236,plain, % 63.05/63.14 (~P1(f7(a4,a1),a1)), % 63.05/63.14 inference(scs_inference,[],[3233,91])). % 63.05/63.14 cnf(3243,plain, % 63.05/63.14 ($false), % 63.05/63.14 inference(scs_inference,[],[3236,3218,532,17]), % 63.05/63.14 ['proof']). % 63.05/63.14 % SZS output end Proof % 63.05/63.14 % Total time :62.480000s %------------------------------------------------------------------------------