%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : COM001-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 : n026.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 04:52:40 EDT 2024 % Result : Unsatisfiable 58.59s 58.72s % Output : CNFRefutation 59.35s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : COM001-1 : TPTP v8.2.0. Released v1.0.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n026.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Thu Jun 20 23:18:54 EDT 2024 % 0.12/0.33 % CPUTime : % 0.50/0.59 start to proof:theBenchmark % 58.59/58.70 %------------------------------------------- % 58.59/58.70 % File :CSE---1.7 % 58.59/58.70 % Problem :theBenchmark % 58.59/58.70 % Transform :cnf % 58.59/58.70 % Format :tptp:raw % 58.59/58.70 % Command :java -jar mcs_scs.jar %d %s % 58.59/58.70 % 58.59/58.70 % Result :Theorem 58.000000s % 58.59/58.70 % Output :CNFRefutation 58.000000s % 58.59/58.70 %------------------------------------------- % 58.59/58.72 %-------------------------------------------------------------------------- % 58.59/58.72 % File : COM001-1 : TPTP v8.2.0. Released v1.0.0. % 58.59/58.72 % Domain : Computing Theory % 58.59/58.72 % Problem : A program correctness theorem % 58.59/58.72 % Version : Especial. % 58.59/58.72 % English : A simple computing state space, with four states - P3, P4, % 58.59/58.72 % P5, and P8 (the full version of this state space is in the % 58.59/58.72 % problem COM002-1). There is a branch at P3 such that the % 58.59/58.72 % following state is either P4 or P8. P8 has a loop back to P3, % 58.59/58.72 % while P4 leads to termination. The problem is to show that % 58.59/58.72 % there is a loop in the computation, passing through P3. % 58.59/58.72 % 58.59/58.72 % Refs : [RR+72] Reboh et al. (1972), Study of automatic theorem provin % 58.59/58.72 % : [WM76] Wilson & Minker (1976), Resolution, Refinements, and S % 58.59/58.72 % Source : [SPRFN] % 58.59/58.72 % Names : SHORTBURST [RR+72] % 58.59/58.72 % : SHORTBURST [WM76] % 58.59/58.72 % 58.59/58.72 % Status : Unsatisfiable % 58.59/58.72 % Rating : 0.00 v5.4.0, 0.06 v5.3.0, 0.05 v5.2.0, 0.00 v2.0.0 % 58.59/58.72 % Syntax : Number of clauses : 11 ( 7 unt; 0 nHn; 11 RR) % 58.59/58.72 % Number of literals : 17 ( 0 equ; 7 neg) % 58.59/58.72 % Maximal clause size : 3 ( 1 avg) % 58.59/58.72 % Maximal term depth : 3 ( 1 avg) % 58.59/58.72 % Number of predicates : 4 ( 4 usr; 0 prp; 2-2 aty) % 58.59/58.72 % Number of functors : 11 ( 11 usr; 8 con; 0-2 aty) % 58.59/58.72 % Number of variables : 11 ( 1 sgn) % 58.59/58.72 % SPC : CNF_UNS_RFO_NEQ_HRN % 58.59/58.72 % 58.59/58.72 % Comments : I suspect this problem was originally by R.M. Burstall. % 58.59/58.72 %-------------------------------------------------------------------------- % 58.59/58.72 cnf(direct_success,axiom, % 58.59/58.72 ( succeeds(Goal_state,Start_state) % 58.59/58.72 | ~ follows(Goal_state,Start_state) ) ). % 58.59/58.72 % 58.59/58.72 cnf(transitivity_of_success,axiom, % 58.59/58.72 ( succeeds(Goal_state,Start_state) % 58.59/58.72 | ~ succeeds(Goal_state,Intermediate_state) % 58.59/58.72 | ~ succeeds(Intermediate_state,Start_state) ) ). % 58.59/58.72 % 58.59/58.72 cnf(goto_success,axiom, % 58.59/58.72 ( succeeds(Goal_state,Start_state) % 58.59/58.72 | ~ has(Start_state,goto(Label)) % 58.59/58.72 | ~ labels(Label,Goal_state) ) ). % 58.59/58.72 % 58.59/58.72 cnf(conditional_success,axiom, % 58.59/58.72 ( succeeds(Goal_state,Start_state) % 58.59/58.72 | ~ has(Start_state,ifthen(Condition,Goal_state)) ) ). % 58.59/58.72 % 58.59/58.72 cnf(label_state_3,hypothesis, % 58.59/58.72 labels(loop,p3) ). % 58.59/58.72 % 58.59/58.72 cnf(state_3,hypothesis, % 58.59/58.72 has(p3,ifthen(equal_function(register_j,n),p4)) ). % 58.59/58.72 % 58.59/58.72 cnf(state_4,hypothesis, % 58.59/58.72 has(p4,goto(out)) ). % 58.59/58.72 % 58.59/58.72 cnf(transition_4_to_5,hypothesis, % 58.59/58.72 follows(p5,p4) ). % 58.59/58.72 % 58.59/58.72 cnf(transition_3_to_8,hypothesis, % 58.59/58.72 follows(p8,p3) ). % 58.59/58.72 % 58.59/58.72 cnf(state_8,hypothesis, % 58.59/58.72 has(p8,goto(loop)) ). % 58.59/58.72 % 58.59/58.72 cnf(prove_there_is_a_loop_through_p3,negated_conjecture, % 58.59/58.72 ~ succeeds(p3,p3) ). % 58.59/58.72 % 58.59/58.72 %-------------------------------------------------------------------------- % 58.59/58.72 %------------------------------------------- % 58.59/58.72 % Proof found % 58.59/58.72 % SZS status Theorem for theBenchmark % 58.59/58.72 % SZS output start Proof % 58.59/58.74 %ClaNum:11(EqnAxiom:0) % 58.59/58.74 %VarNum:21(SingletonVarNum:11) % 58.59/58.74 %MaxLitNum:3 % 58.59/58.74 %MaxfuncDepth:2 % 58.59/58.74 %SharedTerms:19 % 58.59/58.74 %goalClause: 7 % 58.59/58.74 %singleGoalClaCount:1 % 58.59/58.74 [1]P1(a1,a2) % 58.59/58.74 [2]P1(a10,a3) % 58.59/58.74 [3]P2(a4,a3) % 58.59/58.74 [7]~P4(a3,a3) % 58.59/58.74 [4]P3(a2,f5(a8)) % 58.59/58.74 [5]P3(a10,f5(a4)) % 58.59/58.74 [6]P3(a3,f7(f6(a11,a9),a2)) % 58.59/58.75 [8]~P1(x81,x82)+P4(x81,x82) % 58.59/58.75 [11]P4(x111,x112)+~P3(x112,f7(x113,x111)) % 58.59/58.75 [9]~P4(x91,x93)+P4(x91,x92)+~P4(x93,x92) % 58.59/58.75 [10]P4(x101,x102)+~P2(x103,x101)+~P3(x102,f5(x103)) % 58.59/58.75 %EqnAxiom % 58.59/58.75 % 58.59/58.75 %------------------------------------------- % 59.02/59.13 cnf(22,plain, % 59.02/59.13 (P4(a3,a10)), % 59.02/59.13 inference(scs_inference,[],[7,3,5,8,10])). % 59.02/59.13 cnf(422708,plain, % 59.02/59.13 ($false), % 59.02/59.13 inference(scs_inference,[],[7,22,2,8,9]), % 59.02/59.13 ['proof']). % 59.35/59.43 % SZS output end Proof % 59.35/59.43 % Total time :58.000000s %------------------------------------------------------------------------------