%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : RNG001-3 : TPTP v8.2.0. Released v1.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n002.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:00:33 EDT 2024 % Result : Unsatisfiable 11.02s 11.09s % Output : CNFRefutation 11.02s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : RNG001-3 : TPTP v8.2.0. Released v1.0.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n002.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:42:54 EDT 2024 % 0.12/0.34 % CPUTime : % 0.54/0.58 start to proof:theBenchmark % 11.02/11.08 %------------------------------------------- % 11.02/11.08 % File :CSE---1.7 % 11.02/11.08 % Problem :theBenchmark % 11.02/11.08 % Transform :cnf % 11.02/11.08 % Format :tptp:raw % 11.02/11.08 % Command :java -jar mcs_scs.jar %d %s % 11.02/11.08 % 11.02/11.08 % Result :Theorem 10.460000s % 11.02/11.08 % Output :CNFRefutation 10.460000s % 11.02/11.08 %------------------------------------------- % 11.02/11.08 %-------------------------------------------------------------------------- % 11.02/11.08 % File : RNG001-3 : TPTP v8.2.0. Released v1.0.0. % 11.02/11.08 % Domain : Ring Theory % 11.02/11.08 % Problem : X.additive_identity = additive_identity for any X % 11.02/11.08 % Version : [FL+74] axioms : Incomplete. % 11.02/11.08 % English : % 11.02/11.08 % 11.02/11.08 % Refs : [FL+74] Fleisig et al. (1974), An Implementation of the Model % 11.02/11.08 % : [WM76] Wilson & Minker (1976), Resolution, Refinements, and S % 11.02/11.08 % Source : [SPRFN] % 11.02/11.08 % Names : Example 6a [FL+74] % 11.02/11.08 % : EX6-T? [WM76] % 11.02/11.08 % : ex6.lop [SETHEO] % 11.02/11.08 % : FEX6T1 [SPRFN] % 11.02/11.08 % : FEX6T2 [SPRFN] % 11.02/11.08 % 11.02/11.08 % Status : Unsatisfiable % 11.02/11.08 % Rating : 0.18 v8.2.0, 0.14 v8.1.0, 0.00 v7.4.0, 0.17 v7.3.0, 0.00 v6.1.0, 0.07 v6.0.0, 0.11 v5.5.0, 0.06 v5.4.0, 0.17 v5.3.0, 0.25 v5.2.0, 0.08 v5.1.0, 0.06 v5.0.0, 0.07 v4.0.1, 0.14 v4.0.0, 0.29 v3.4.0, 0.40 v3.3.0, 0.00 v2.7.0, 0.12 v2.6.0, 0.14 v2.5.0, 0.00 v2.4.0, 0.14 v2.3.0, 0.14 v2.2.1, 0.22 v2.1.0, 0.14 v2.0.0 % 11.02/11.08 % Syntax : Number of clauses : 8 ( 4 unt; 0 nHn; 5 RR) % 11.02/11.08 % Number of literals : 22 ( 0 equ; 15 neg) % 11.02/11.08 % Maximal clause size : 5 ( 2 avg) % 11.02/11.08 % Maximal term depth : 2 ( 1 avg) % 11.02/11.08 % Number of predicates : 2 ( 2 usr; 0 prp; 3-3 aty) % 11.02/11.08 % Number of functors : 4 ( 4 usr; 2 con; 0-2 aty) % 11.02/11.08 % Number of variables : 30 ( 0 sgn) % 11.02/11.08 % SPC : CNF_UNS_RFO_NEQ_HRN % 11.02/11.08 % 11.02/11.08 % Comments : % 11.02/11.08 %-------------------------------------------------------------------------- % 11.02/11.08 cnf(additive_identity1,axiom, % 11.02/11.08 sum(additive_identity,X,X) ). % 11.02/11.08 % 11.02/11.08 cnf(additive_inverse1,axiom, % 11.02/11.08 sum(additive_inverse(X),X,additive_identity) ). % 11.02/11.08 % 11.02/11.08 cnf(associativity_of_addition1,axiom, % 11.02/11.08 ( ~ sum(X,Y,U) % 11.02/11.08 | ~ sum(Y,Z,V) % 11.02/11.08 | ~ sum(U,Z,W) % 11.02/11.08 | sum(X,V,W) ) ). % 11.02/11.08 % 11.02/11.08 cnf(associativity_of_addition2,axiom, % 11.02/11.08 ( ~ sum(X,Y,U) % 11.02/11.08 | ~ sum(Y,Z,V) % 11.02/11.08 | ~ sum(X,V,W) % 11.02/11.08 | sum(U,Z,W) ) ). % 11.02/11.08 % 11.02/11.08 cnf(closure_of_multiplication,axiom, % 11.02/11.08 product(X,Y,multiply(X,Y)) ). % 11.02/11.08 % 11.02/11.08 cnf(distributivity1,axiom, % 11.02/11.08 ( ~ product(X,Y,V1) % 11.02/11.08 | ~ product(X,Z,V2) % 11.02/11.08 | ~ sum(Y,Z,V3) % 11.02/11.08 | ~ product(X,V3,V4) % 11.02/11.08 | sum(V1,V2,V4) ) ). % 11.02/11.08 % 11.02/11.08 cnf(distributivity2,axiom, % 11.02/11.08 ( ~ product(X,Y,V1) % 11.02/11.08 | ~ product(X,Z,V2) % 11.02/11.08 | ~ sum(Y,Z,V3) % 11.02/11.08 | ~ sum(V1,V2,V4) % 11.02/11.08 | product(X,V3,V4) ) ). % 11.02/11.09 % 11.02/11.09 cnf(prove_a_times_additive_id_is_additive_id,negated_conjecture, % 11.02/11.09 ~ product(a,additive_identity,additive_identity) ). % 11.02/11.09 % 11.02/11.09 %-------------------------------------------------------------------------- % 11.02/11.09 %------------------------------------------- % 11.02/11.09 % Proof found % 11.02/11.09 % SZS status Theorem for theBenchmark % 11.02/11.09 % SZS output start Proof % 11.02/11.09 %ClaNum:8(EqnAxiom:0) % 11.02/11.09 %VarNum:62(SingletonVarNum:30) % 11.02/11.09 %MaxLitNum:5 % 11.02/11.09 %MaxfuncDepth:1 % 11.02/11.09 %SharedTerms:3 % 11.02/11.09 %goalClause: 4 % 11.02/11.09 %singleGoalClaCount:1 % 11.02/11.09 [4]~P2(a2,a1,a1) % 11.02/11.09 [1]P1(a1,x11,x11) % 11.02/11.09 [2]P1(f3(x21),x21,a1) % 11.02/11.09 [3]P2(x31,x32,f4(x31,x32)) % 11.02/11.09 [5]~P1(x56,x54,x51)+P1(x51,x52,x53)+~P1(x54,x52,x55)+~P1(x56,x55,x53) % 11.02/11.09 [6]~P1(x61,x66,x64)+P1(x61,x62,x63)+~P1(x64,x65,x63)+~P1(x66,x65,x62) % 11.02/11.09 [7]~P2(x77,x75,x72)+~P2(x77,x74,x71)+P1(x71,x72,x73)+~P1(x74,x75,x76)+~P2(x77,x76,x73) % 11.02/11.09 [8]~P2(x81,x87,x85)+~P2(x81,x86,x84)+P2(x81,x82,x83)+~P1(x84,x85,x83)+~P1(x86,x87,x82) % 11.02/11.09 %EqnAxiom % 11.02/11.09 % 11.02/11.09 %------------------------------------------- % 11.02/11.09 cnf(11,plain, % 11.02/11.09 (P1(a1,x111,x111)), % 11.02/11.09 inference(rename_variables,[],[1])). % 11.02/11.09 cnf(12,plain, % 11.02/11.09 (P2(x121,x122,f4(x121,x122))), % 11.02/11.09 inference(rename_variables,[],[3])). % 11.02/11.09 cnf(14,plain, % 11.02/11.09 (P1(f4(x141,a1),f4(x141,a1),f4(x141,a1))), % 11.02/11.09 inference(scs_inference,[],[4,1,11,3,12,2,8,7])). % 11.02/11.09 cnf(20,plain, % 11.02/11.09 (P1(a1,f4(x201,a1),a1)), % 11.02/11.09 inference(scs_inference,[],[14,2,5])). % 11.02/11.09 cnf(26,plain, % 11.02/11.09 (P1(f3(a1),x261,x261)), % 11.02/11.09 inference(scs_inference,[],[2,1,6])). % 11.02/11.09 cnf(31,plain, % 11.02/11.09 (P1(f3(f3(a1)),x311,x311)), % 11.02/11.09 inference(scs_inference,[],[2,1,26,6])). % 11.02/11.09 cnf(40,plain, % 11.02/11.09 (P1(f3(a1),f4(x401,a1),a1)), % 11.02/11.09 inference(scs_inference,[],[2,20,1,6])). % 11.02/11.09 cnf(60,plain, % 11.02/11.09 (P1(a1,f3(a1),a1)), % 11.02/11.09 inference(scs_inference,[],[1,2,31,6])). % 11.02/11.09 cnf(86,plain, % 11.02/11.09 (P1(f3(a1),a1,f3(a1))), % 11.02/11.09 inference(scs_inference,[],[26,31,2,6])). % 11.02/11.09 cnf(87,plain, % 11.02/11.09 (P1(f3(x871),x871,a1)), % 11.02/11.09 inference(rename_variables,[],[2])). % 11.02/11.09 cnf(88,plain, % 11.02/11.09 (P1(f3(a1),x881,x881)), % 11.02/11.09 inference(rename_variables,[],[26])). % 11.02/11.09 cnf(96,plain, % 11.02/11.09 (P1(f3(a1),f4(x961,a1),f3(a1))), % 11.02/11.09 inference(scs_inference,[],[26,88,4,20,31,2,87,3,6,8,5])). % 11.02/11.09 cnf(729,plain, % 11.02/11.09 (P1(a1,a1,f3(a1))), % 11.02/11.09 inference(scs_inference,[],[86,1,26,6])). % 11.02/11.09 cnf(851,plain, % 11.02/11.09 (P1(f3(f3(a1)),a1,f3(a1))), % 11.02/11.09 inference(scs_inference,[],[86,31,26,6])). % 11.02/11.09 cnf(994,plain, % 11.02/11.09 (P1(a1,f4(x9941,a1),f3(a1))), % 11.02/11.09 inference(scs_inference,[],[96,729,1,6])). % 11.02/11.09 cnf(998,plain, % 11.02/11.09 (P1(f3(x9981),x9981,a1)), % 11.02/11.09 inference(rename_variables,[],[2])). % 11.02/11.09 cnf(1000,plain, % 11.02/11.09 (~P2(x10001,f3(a1),x10002)+P1(x10002,f4(x10001,a1),f4(x10001,a1))), % 11.02/11.09 inference(scs_inference,[],[96,729,2,998,1,3,6,5,7])). % 11.02/11.09 cnf(1006,plain, % 11.02/11.09 (P1(f4(x10061,f3(a1)),f4(x10061,a1),f4(x10061,a1))), % 11.02/11.09 inference(scs_inference,[],[3,1000])). % 11.02/11.09 cnf(1387,plain, % 11.02/11.09 (P1(f3(a1),f3(a1),a1)), % 11.02/11.09 inference(scs_inference,[],[851,2,1,5])). % 11.02/11.09 cnf(1391,plain, % 11.02/11.09 (~P2(a2,f3(a1),f3(a1))), % 11.02/11.09 inference(scs_inference,[],[851,4,2,1,5,8])). % 11.02/11.09 cnf(3525,plain, % 11.02/11.09 (~P2(x35251,f3(a1),x35252)+P1(f4(x35251,a1),f4(x35251,a1),x35252)), % 11.02/11.09 inference(scs_inference,[],[3,729,7])). % 11.02/11.09 cnf(3536,plain, % 11.02/11.09 (P1(f4(x35361,a1),f4(x35361,a1),f4(x35361,f3(a1)))), % 11.02/11.09 inference(scs_inference,[],[3,3525])). % 11.02/11.09 cnf(3743,plain, % 11.02/11.09 (P1(f4(x37431,a1),f4(x37431,f3(a1)),f4(x37431,a1))), % 11.02/11.09 inference(scs_inference,[],[1006,3536,6])). % 11.02/11.09 cnf(3762,plain, % 11.02/11.09 (P1(f3(a1),f4(x37621,a1),f4(x37621,f3(a1)))), % 11.02/11.09 inference(scs_inference,[],[40,1,3743,6])). % 11.02/11.09 cnf(3768,plain, % 11.02/11.09 (P1(a1,f4(x37681,f3(a1)),a1)), % 11.02/11.09 inference(scs_inference,[],[60,20,3762,6])). % 11.02/11.09 cnf(3938,plain, % 11.02/11.09 (P1(f3(a1),a1,f4(x39381,f3(a1)))), % 11.02/11.09 inference(scs_inference,[],[86,26,3768,6])). % 11.02/11.09 cnf(3943,plain, % 11.02/11.09 (P1(f3(a1),f4(x39431,f3(a1)),f3(a1))), % 11.02/11.09 inference(scs_inference,[],[1387,729,3938,6])). % 11.02/11.09 cnf(3947,plain, % 11.02/11.09 (P1(f3(a1),f3(a1),f4(x39471,f3(a1)))), % 11.02/11.09 inference(scs_inference,[],[1387,1,3943,6])). % 11.02/11.09 cnf(4025,plain, % 11.02/11.09 (P1(a1,a1,f4(x40251,f3(a1)))), % 11.02/11.09 inference(scs_inference,[],[26,1387,3938,5])). % 11.02/11.09 cnf(4028,plain, % 11.02/11.09 (P1(a1,f4(x40281,f3(a1)),x40282)+~P1(f4(x40281,f3(a1)),a1,x40282)), % 11.02/11.09 inference(scs_inference,[],[26,1387,3938,5,6])). % 11.02/11.09 cnf(4065,plain, % 11.02/11.09 (P1(x40651,f4(x40652,a1),f3(a1))+~P1(f4(x40652,f3(a1)),a1,x40651)), % 11.02/11.09 inference(scs_inference,[],[994,1006,4028,5])). % 11.02/11.09 cnf(4096,plain, % 11.02/11.09 (~P2(a2,f3(a1),x40961)+~P1(f4(a2,f3(a1)),a1,x40961)), % 11.02/11.09 inference(scs_inference,[],[1391,86,3,4065,8])). % 11.02/11.09 cnf(4127,plain, % 11.02/11.09 (~P1(f4(a2,f3(a1)),f3(a1),a1)), % 11.02/11.09 inference(scs_inference,[],[3,26,4025,4096,6])). % 11.02/11.09 cnf(4128,plain, % 11.02/11.09 ($false), % 11.02/11.10 inference(scs_inference,[],[26,1387,3947,4127,5]), % 11.02/11.10 ['proof']). % 11.02/11.10 % SZS output end Proof % 11.02/11.10 % Total time :10.460000s %------------------------------------------------------------------------------