%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SWV019-1 : TPTP v8.2.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n022.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 16:45:30 EDT 2024 % Result : Unsatisfiable 15.94s 16.00s % Output : CNFRefutation 15.94s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : SWV019-1 : TPTP v8.2.0. Released v2.4.0. % 0.10/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.11/0.32 % Computer : n022.cluster.edu % 0.11/0.32 % Model : x86_64 x86_64 % 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.32 % Memory : 8042.1875MB % 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.32 % CPULimit : 300 % 0.11/0.32 % WCLimit : 300 % 0.11/0.32 % DateTime : Thu Jun 20 15:12:09 EDT 2024 % 0.11/0.33 % CPUTime : % 0.19/0.55 start to proof:theBenchmark % 15.92/15.99 %------------------------------------------- % 15.92/15.99 % File :CSE---1.7 % 15.92/15.99 % Problem :theBenchmark % 15.92/15.99 % Transform :cnf % 15.92/15.99 % Format :tptp:raw % 15.92/15.99 % Command :java -jar mcs_scs.jar %d %s % 15.92/15.99 % 15.92/15.99 % Result :Theorem 15.400000s % 15.92/15.99 % Output :CNFRefutation 15.400000s % 15.92/15.99 %------------------------------------------- % 15.94/15.99 %-------------------------------------------------------------------------- % 15.94/15.99 % File : SWV019-1 : TPTP v8.2.0. Released v2.4.0. % 15.94/15.99 % Domain : Software Verification % 15.94/15.99 % Problem : Maximal array element % 15.94/15.99 % Version : [Ver93] axioms : Incomplete. % 15.94/15.99 % English : % 15.94/15.99 % 15.94/15.99 % Refs : [Ver93] Veroff (1993), Email to G. Sutcliffe % 15.94/15.99 % Source : [Ver93] % 15.94/15.99 % Names : % 15.94/15.99 % 15.94/15.99 % Status : Unsatisfiable % 15.94/15.99 % Rating : 0.05 v8.1.0, 0.00 v7.0.0, 0.07 v6.4.0, 0.00 v6.1.0, 0.07 v6.0.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.4.0 % 15.94/15.99 % Syntax : Number of clauses : 10 ( 5 unt; 2 nHn; 8 RR) % 15.94/15.99 % Number of literals : 22 ( 2 equ; 11 neg) % 15.94/15.99 % Maximal clause size : 7 ( 2 avg) % 15.94/15.99 % Maximal term depth : 2 ( 1 avg) % 15.94/15.99 % Number of predicates : 3 ( 2 usr; 0 prp; 2-2 aty) % 15.94/15.99 % Number of functors : 8 ( 8 usr; 6 con; 0-2 aty) % 15.94/15.99 % Number of variables : 7 ( 0 sgn) % 15.94/15.99 % SPC : CNF_UNS_RFO_SEQ_NHN % 15.94/15.99 % 15.94/15.99 % Comments : [Ver93] says "Only the clauses needed for the proof are included. % 15.94/15.99 % What makes the problem interesting/challenging from a theorem % 15.94/15.99 % proving perspective is the addition of standard sets of axioms % 15.94/15.99 % (that don't participate in the proof, but sure get in the way % 15.94/15.99 % of finding the proof). % 15.94/15.99 %-------------------------------------------------------------------------- % 15.94/15.99 cnf(in_bounds,axiom, % 15.94/15.99 ( less_than(X1,lower_bound) % 15.94/15.99 | less_than(upper_bound,X1) % 15.94/15.99 | in_array_bounds(array,X1) ) ). % 15.94/15.99 % 15.94/15.99 cnf(predecessor_less,axiom, % 15.94/15.99 ( ~ less_than(successor(X),successor(Y)) % 15.94/15.99 | less_than(X,Y) ) ). % 15.94/15.99 % 15.94/15.99 cnf(transitivity_of_less,axiom, % 15.94/15.99 ( ~ less_than(X,Y) % 15.94/15.99 | ~ less_than(Y,Z) % 15.94/15.99 | less_than(X,Z) ) ). % 15.94/15.99 % 15.94/15.99 cnf(successor_greater,axiom, % 15.94/15.99 less_than(X,successor(X)) ). % 15.94/15.99 % 15.94/15.99 cnf(this_is_maximal,axiom, % 15.94/15.99 ( ~ in_array_bounds(array,index_of_maximal) % 15.94/15.99 | maximal_value = array_value_at(array,index_of_maximal) ) ). % 15.94/15.99 % 15.94/15.99 cnf(maximal_before_somewhere,axiom, % 15.94/16.00 less_than(index_of_maximal,an_index) ). % 15.94/16.00 % 15.94/16.00 cnf(somewhere_above_lower_bound,axiom, % 15.94/16.00 ~ less_than(an_index,lower_bound) ). % 15.94/16.00 % 15.94/16.00 cnf(somewhere_below_upper_bound,axiom, % 15.94/16.00 ~ less_than(upper_bound,an_index) ). % 15.94/16.00 % 15.94/16.00 cnf(maximal_above_lower_bound,axiom, % 15.94/16.00 ~ less_than(index_of_maximal,lower_bound) ). % 15.94/16.00 % 15.94/16.00 cnf(prove_this,negated_conjecture, % 15.94/16.00 ( ~ in_array_bounds(array,an_index) % 15.94/16.00 | less_than(successor(an_index),lower_bound) % 15.94/16.00 | less_than(successor(upper_bound),successor(an_index)) % 15.94/16.00 | less_than(index_of_maximal,lower_bound) % 15.94/16.00 | ~ less_than(index_of_maximal,successor(an_index)) % 15.94/16.00 | ~ in_array_bounds(array,index_of_maximal) % 15.94/16.00 | maximal_value != array_value_at(array,index_of_maximal) ) ). % 15.94/16.00 % 15.94/16.00 %-------------------------------------------------------------------------- % 15.94/16.00 %------------------------------------------- % 15.94/16.00 % Proof found % 15.94/16.00 % SZS status Theorem for theBenchmark % 15.94/16.00 % SZS output start Proof % 15.94/16.00 %ClaNum:20(EqnAxiom:10) % 15.94/16.00 %VarNum:15(SingletonVarNum:7) % 15.94/16.00 %MaxLitNum:7 % 15.94/16.00 %MaxfuncDepth:1 % 15.94/16.00 %SharedTerms:21 % 15.94/16.00 %goalClause: 20 % 15.94/16.00 [11]P1(a1,a2) % 15.94/16.00 [13]~P1(a8,a2) % 15.94/16.00 [14]~P1(a1,a6) % 15.94/16.00 [15]~P1(a2,a6) % 15.94/16.00 [12]P1(x121,f5(x121)) % 15.94/16.00 [16]~P2(a3,a1)+E(f4(a3,a1),a7) % 15.94/16.00 [18]P1(x181,x182)+~P1(f5(x181),f5(x182)) % 15.94/16.00 [17]P1(a8,x171)+P2(a3,x171)+P1(x171,a6) % 15.94/16.00 [19]~P1(x191,x193)+P1(x191,x192)+~P1(x193,x192) % 15.94/16.00 [20]~P2(a3,a1)+P1(a1,a6)+P1(f5(a8),f5(a2))+~P2(a3,a2)+~E(f4(a3,a1),a7)+P1(f5(a2),a6)+~P1(a1,f5(a2)) % 15.94/16.00 %EqnAxiom % 15.94/16.00 [1]E(x11,x11) % 15.94/16.00 [2]E(x22,x21)+~E(x21,x22) % 15.94/16.00 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 15.94/16.00 [4]~E(x41,x42)+E(f5(x41),f5(x42)) % 15.94/16.00 [5]~E(x51,x52)+E(f4(x51,x53),f4(x52,x53)) % 15.94/16.00 [6]~E(x61,x62)+E(f4(x63,x61),f4(x63,x62)) % 15.94/16.00 [7]P1(x72,x73)+~E(x71,x72)+~P1(x71,x73) % 15.94/16.00 [8]P1(x83,x82)+~E(x81,x82)+~P1(x83,x81) % 15.94/16.00 [9]P2(x92,x93)+~E(x91,x92)+~P2(x91,x93) % 15.94/16.00 [10]P2(x103,x102)+~E(x101,x102)+~P2(x103,x101) % 15.94/16.00 % 15.94/16.00 %------------------------------------------- % 15.94/16.00 cnf(21,plain, % 15.94/16.00 (~P1(a8,a1)), % 15.94/16.00 inference(scs_inference,[],[11,13,19])). % 15.94/16.00 cnf(25,plain, % 15.94/16.00 (~P2(a3,a1)+P1(f5(a8),f5(a2))+~P2(a3,a2)+~E(f4(a3,a1),a7)+P1(f5(a2),a6)+~P1(a1,f5(a2))), % 15.94/16.00 inference(scs_inference,[],[14,20])). % 15.94/16.00 cnf(27,plain, % 15.94/16.00 (P1(x271,f5(x271))), % 15.94/16.00 inference(rename_variables,[],[12])). % 15.94/16.00 cnf(28,plain, % 15.94/16.00 (P1(a1,f5(a2))), % 15.94/16.00 inference(scs_inference,[],[11,21,12,27,8,19])). % 15.94/16.00 cnf(40,plain, % 15.94/16.00 (~P2(a3,a1)+P1(f5(a8),f5(a2))+~P2(a3,a2)+~E(f4(a3,a1),a7)+P1(f5(a2),a6)), % 15.94/16.00 inference(scs_inference,[],[28,25])). % 15.94/16.00 cnf(56,plain, % 15.94/16.00 (E(f4(a3,a1),a7)), % 15.94/16.00 inference(scs_inference,[],[14,21,16,17])). % 15.94/16.00 cnf(57,plain, % 15.94/16.00 (~P2(a3,a1)+P1(f5(a8),f5(a2))+~P2(a3,a2)+P1(f5(a2),a6)), % 15.94/16.00 inference(scs_inference,[],[56,40])). % 15.94/16.00 cnf(1307,plain, % 15.94/16.00 (~P2(a3,a1)+~P2(a3,a2)+P1(f5(a2),a6)), % 15.94/16.00 inference(scs_inference,[],[13,18,57])). % 15.94/16.00 cnf(1308,plain, % 15.94/16.00 (~P2(a3,a2)+P1(f5(a2),a6)), % 15.94/16.00 inference(scs_inference,[],[21,14,1307,17])). % 15.94/16.00 cnf(1309,plain, % 15.94/16.00 (P1(f5(a2),a6)), % 15.94/16.00 inference(scs_inference,[],[13,15,1308,17])). % 15.94/16.00 cnf(1310,plain, % 15.94/16.00 ($false), % 15.94/16.00 inference(scs_inference,[],[1309,28,14,19]), % 15.94/16.00 ['proof']). % 15.94/16.00 % SZS output end Proof % 15.94/16.00 % Total time :15.400000s %------------------------------------------------------------------------------