%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SET016-1 : TPTP v8.2.0. Released v1.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n028.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:03 EDT 2024 % Result : Unsatisfiable 5.53s 5.65s % Output : CNFRefutation 5.53s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.05/0.10 % Problem : SET016-1 : TPTP v8.2.0. Released v1.0.0. % 0.05/0.10 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.10/0.30 % Computer : n028.cluster.edu % 0.10/0.30 % Model : x86_64 x86_64 % 0.10/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.30 % Memory : 8042.1875MB % 0.10/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.30 % CPULimit : 300 % 0.10/0.30 % WCLimit : 300 % 0.10/0.30 % DateTime : Sun Jun 23 15:12:08 EDT 2024 % 0.10/0.30 % CPUTime : % 0.15/0.51 start to proof:theBenchmark % 5.53/5.64 %------------------------------------------- % 5.53/5.64 % File :CSE---1.7 % 5.53/5.64 % Problem :theBenchmark % 5.53/5.64 % Transform :cnf % 5.53/5.64 % Format :tptp:raw % 5.53/5.64 % Command :java -jar mcs_scs.jar %d %s % 5.53/5.64 % 5.53/5.64 % Result :Theorem 5.100000s % 5.53/5.64 % Output :CNFRefutation 5.100000s % 5.53/5.64 %------------------------------------------- % 5.53/5.65 %-------------------------------------------------------------------------- % 5.53/5.65 % File : SET016-1 : TPTP v8.2.0. Released v1.0.0. % 5.53/5.65 % Domain : Set Theory % 5.53/5.65 % Problem : First components of equal ordered pairs are equal % 5.53/5.65 % Version : [LW91] axioms : Incomplete. % 5.53/5.65 % English : % 5.53/5.65 % 5.53/5.65 % Refs : [LW91] Lusk & Wos (1991), Benchmark Problems in Which Equalit % 5.53/5.65 % : [LW92] Lusk & Wos (1992), Benchmark Problems in Which Equalit % 5.53/5.65 % Source : [LW91] % 5.53/5.65 % Names : NU3.1 [LW92] % 5.53/5.65 % 5.53/5.65 % Status : Unsatisfiable % 5.53/5.65 % 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.3.0, 0.09 v6.2.0, 0.10 v6.1.0, 0.21 v6.0.0, 0.10 v5.5.0, 0.25 v5.4.0, 0.20 v5.3.0, 0.22 v5.2.0, 0.06 v5.1.0, 0.12 v5.0.0, 0.07 v4.1.0, 0.08 v4.0.1, 0.18 v3.7.0, 0.10 v3.5.0, 0.09 v3.4.0, 0.17 v3.3.0, 0.14 v3.2.0, 0.23 v3.1.0, 0.18 v2.7.0, 0.25 v2.6.0, 0.10 v2.5.0, 0.25 v2.4.0, 0.11 v2.3.0, 0.22 v2.2.1, 0.22 v2.2.0, 0.33 v2.1.0, 0.33 v2.0.0 % 5.53/5.65 % Syntax : Number of clauses : 8 ( 6 unt; 1 nHn; 4 RR) % 5.53/5.65 % Number of literals : 11 ( 6 equ; 3 neg) % 5.53/5.65 % Maximal clause size : 3 ( 1 avg) % 5.53/5.65 % Maximal term depth : 3 ( 1 avg) % 5.53/5.65 % Number of predicates : 2 ( 1 usr; 0 prp; 2-2 aty) % 5.53/5.65 % Number of functors : 7 ( 7 usr; 4 con; 0-2 aty) % 5.53/5.65 % Number of variables : 12 ( 2 sgn) % 5.53/5.65 % SPC : CNF_UNS_RFO_SEQ_NHN % 5.53/5.65 % 5.53/5.65 % Comments : % 5.53/5.65 %-------------------------------------------------------------------------- % 5.53/5.65 cnf(singleton_1,axiom, % 5.53/5.65 member(X,singleton_set(X)) ). % 5.53/5.65 % 5.53/5.65 cnf(singleton_2,axiom, % 5.53/5.65 ( ~ member(X,singleton_set(Y)) % 5.53/5.65 | X = Y ) ). % 5.53/5.65 % 5.53/5.65 cnf(unordered_pair_1,axiom, % 5.53/5.65 member(X,unordered_pair(X,Y)) ). % 5.53/5.65 % 5.53/5.65 cnf(unordered_pair_2,axiom, % 5.53/5.65 member(Y,unordered_pair(X,Y)) ). % 5.53/5.65 % 5.53/5.65 cnf(unordered_pair_3,axiom, % 5.53/5.65 ( ~ member(X,unordered_pair(Y,Z)) % 5.53/5.65 | X = Y % 5.53/5.65 | X = Z ) ). % 5.53/5.65 % 5.53/5.65 cnf(ordered_pair,axiom, % 5.53/5.65 ordered_pair(X,Y) = unordered_pair(singleton_set(X),unordered_pair(X,Y)) ). % 5.53/5.65 % 5.53/5.65 cnf(equal_ordered_pairs,hypothesis, % 5.53/5.65 ordered_pair(m1,r1) = ordered_pair(m2,r2) ). % 5.53/5.65 % 5.53/5.65 cnf(prove_first_components_equal,negated_conjecture, % 5.53/5.65 m1 != m2 ). % 5.53/5.65 % 5.53/5.65 %-------------------------------------------------------------------------- % 5.53/5.65 %------------------------------------------- % 5.53/5.65 % Proof found % 5.53/5.65 % SZS status Theorem for theBenchmark % 5.53/5.65 % SZS output start Proof % 5.53/5.66 %ClaNum:15(EqnAxiom:8) % 5.53/5.66 %VarNum:19(SingletonVarNum:10) % 5.53/5.66 %MaxLitNum:3 % 5.53/5.66 %MaxfuncDepth:2 % 5.53/5.66 %SharedTerms:12 % 5.53/5.66 %goalClause: 13 % 5.53/5.66 %singleGoalClaCount:1 % 5.53/5.66 [13]~E(a2,a4) % 5.53/5.66 [12]E(f6(f1(a2),f6(a2,a3)),f6(f1(a4),f6(a4,a5))) % 5.53/5.66 [9]P1(x91,f1(x91)) % 5.53/5.66 [10]P1(x101,f6(x102,x101)) % 5.53/5.66 [11]P1(x111,f6(x111,x112)) % 5.53/5.66 [14]E(x141,x142)+~P1(x141,f1(x142)) % 5.53/5.66 [15]E(x151,x152)+E(x151,x153)+~P1(x151,f6(x153,x152)) % 5.53/5.66 %EqnAxiom % 5.53/5.66 [1]E(x11,x11) % 5.53/5.66 [2]E(x22,x21)+~E(x21,x22) % 5.53/5.66 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 5.53/5.66 [4]~E(x41,x42)+E(f1(x41),f1(x42)) % 5.53/5.66 [5]~E(x51,x52)+E(f6(x51,x53),f6(x52,x53)) % 5.53/5.66 [6]~E(x61,x62)+E(f6(x63,x61),f6(x63,x62)) % 5.53/5.66 [7]P1(x72,x73)+~E(x71,x72)+~P1(x71,x73) % 5.53/5.66 [8]P1(x83,x82)+~E(x81,x82)+~P1(x83,x81) % 5.53/5.66 % 5.53/5.66 %------------------------------------------- % 5.53/5.67 cnf(16,plain, % 5.53/5.67 (E(f6(f1(a4),f6(a4,a5)),f6(f1(a2),f6(a2,a3)))), % 5.53/5.67 inference(scs_inference,[],[12,2])). % 5.53/5.67 cnf(45,plain, % 5.53/5.67 (P1(x451,x452)+~E(f1(x451),x452)), % 5.53/5.67 inference(scs_inference,[],[9,8])). % 5.53/5.67 cnf(53,plain, % 5.53/5.67 (P1(f1(a2),f6(f1(a4),f6(a4,a5)))), % 5.53/5.67 inference(scs_inference,[],[12,11,8])). % 5.53/5.67 cnf(58,plain, % 5.53/5.67 (E(f6(a4,a5),f1(a2))+E(f1(a2),f1(a4))), % 5.53/5.67 inference(scs_inference,[],[12,11,8,15,45,2])). % 5.53/5.67 cnf(61,plain, % 5.53/5.67 (P1(x611,f6(f1(a4),f6(a4,a5)))+~E(f1(a2),x611)), % 5.53/5.67 inference(scs_inference,[],[53,7])). % 5.53/5.67 cnf(62,plain, % 5.53/5.67 (P1(x621,f6(f1(a2),f6(a2,a3)))+~E(f1(a2),x621)), % 5.53/5.67 inference(scs_inference,[],[16,53,7,8])). % 5.53/5.67 cnf(69,plain, % 5.53/5.67 (P1(a5,f1(a2))+E(f1(a2),f1(a4))), % 5.53/5.67 inference(scs_inference,[],[10,58,8])). % 5.53/5.67 cnf(70,plain, % 5.53/5.67 (P1(a2,f1(a4))+P1(a5,f1(a2))), % 5.53/5.67 inference(scs_inference,[],[69,45])). % 5.53/5.67 cnf(71,plain, % 5.53/5.67 (P1(a5,f1(a2))), % 5.53/5.67 inference(scs_inference,[],[13,70,14])). % 5.53/5.67 cnf(72,plain, % 5.53/5.67 (E(a5,a2)), % 5.53/5.67 inference(scs_inference,[],[71,14])). % 5.53/5.67 cnf(158,plain, % 5.53/5.67 (E(f1(a2),f1(a5))), % 5.53/5.67 inference(scs_inference,[],[72,2,4])). % 5.53/5.67 cnf(164,plain, % 5.53/5.67 (E(f1(a2),f1(a4))+E(f1(a5),f6(a4,a5))), % 5.53/5.67 inference(scs_inference,[],[158,61,62,2,15,3])). % 5.53/5.67 cnf(219,plain, % 5.53/5.67 (P1(a2,f1(a4))+E(f1(a5),f6(a4,a5))), % 5.53/5.67 inference(scs_inference,[],[9,164,8])). % 5.53/5.67 cnf(235,plain, % 5.53/5.67 (E(f6(a4,a5),f1(a5))+P1(a2,f1(a4))), % 5.53/5.67 inference(scs_inference,[],[219,2])). % 5.53/5.67 cnf(251,plain, % 5.53/5.67 (E(f6(a4,a5),f1(a5))), % 5.53/5.67 inference(scs_inference,[],[13,235,14])). % 5.53/5.67 cnf(769,plain, % 5.53/5.67 (E(a4,a5)), % 5.53/5.67 inference(scs_inference,[],[251,9,11,7,8,14])). % 5.53/5.67 cnf(781,plain, % 5.53/5.67 (E(a4,a2)), % 5.53/5.67 inference(scs_inference,[],[72,769,2,3])). % 5.53/5.67 cnf(787,plain, % 5.53/5.67 ($false), % 5.53/5.67 inference(scs_inference,[],[13,781,2]), % 5.53/5.67 ['proof']). % 5.53/5.67 % SZS output end Proof % 5.53/5.67 % Total time :5.100000s %------------------------------------------------------------------------------