%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : COM002-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 : n032.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:41 EDT 2024 % Result : Unsatisfiable 58.50s 58.62s % Output : CNFRefutation 58.69s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.11 % Problem : COM002-1 : TPTP v8.2.0. Released v1.0.0. % 0.10/0.11 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.11/0.30 % Computer : n032.cluster.edu % 0.11/0.30 % Model : x86_64 x86_64 % 0.11/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.30 % Memory : 8042.1875MB % 0.11/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.30 % CPULimit : 300 % 0.11/0.30 % WCLimit : 300 % 0.11/0.30 % DateTime : Thu Jun 20 23:37:53 EDT 2024 % 0.11/0.30 % CPUTime : % 0.15/0.53 start to proof:theBenchmark % 58.41/58.60 %------------------------------------------- % 58.41/58.60 % File :CSE---1.7 % 58.41/58.60 % Problem :theBenchmark % 58.41/58.60 % Transform :cnf % 58.41/58.60 % Format :tptp:raw % 58.41/58.60 % Command :java -jar mcs_scs.jar %d %s % 58.41/58.60 % 58.41/58.60 % Result :Theorem 58.010000s % 58.41/58.60 % Output :CNFRefutation 58.010000s % 58.41/58.60 %------------------------------------------- % 58.50/58.62 %-------------------------------------------------------------------------- % 58.50/58.62 % File : COM002-1 : TPTP v8.2.0. Released v1.0.0. % 58.50/58.62 % Domain : Computing Theory % 58.50/58.62 % Problem : A program correctness theorem % 58.50/58.62 % Version : Especial. % 58.50/58.62 % English : A computing state space, with eight states - P1 to P8. % 58.50/58.62 % P1 leads to P3 via P2. There is a branch at P3 such that the % 58.50/58.62 % following state is either P4 or P6. P6 leads to P8, which has % 58.50/58.62 % a loop back to P3, while P4 leads to termination. The problem % 58.50/58.62 % is to show that there is a loop in the computation, passing % 58.50/58.62 % through P3. % 58.50/58.62 % 58.50/58.62 % Refs : [RR+72] Reboh et al. (1972), Study of automatic theorem provin % 58.50/58.62 % : [WM76] Wilson & Minker (1976), Resolution, Refinements, and S % 58.50/58.62 % Source : [SPRFN] % 58.50/58.62 % Names : BURSTALL [RR+72] % 58.50/58.62 % : BURSTALL [WM76] % 58.50/58.62 % 58.50/58.62 % Status : Unsatisfiable % 58.50/58.62 % Rating : 0.00 v5.4.0, 0.06 v5.3.0, 0.10 v5.2.0, 0.00 v2.2.1, 0.11 v2.1.0, 0.00 v2.0.0 % 58.50/58.62 % Syntax : Number of clauses : 19 ( 15 unt; 0 nHn; 19 RR) % 58.50/58.62 % Number of literals : 25 ( 0 equ; 7 neg) % 58.50/58.62 % Maximal clause size : 3 ( 1 avg) % 58.50/58.62 % Maximal term depth : 3 ( 1 avg) % 58.50/58.62 % Number of predicates : 4 ( 4 usr; 0 prp; 2-2 aty) % 58.50/58.62 % Number of functors : 22 ( 22 usr; 16 con; 0-2 aty) % 58.50/58.62 % Number of variables : 11 ( 1 sgn) % 58.50/58.62 % SPC : CNF_UNS_RFO_NEQ_HRN % 58.50/58.62 % 58.50/58.62 % Comments : I suspect this problem was originally by R.M. Burstall. % 58.50/58.62 %-------------------------------------------------------------------------- % 58.50/58.62 cnf(direct_success,axiom, % 58.50/58.62 ( succeeds(Goal_state,Start_state) % 58.50/58.62 | ~ follows(Goal_state,Start_state) ) ). % 58.50/58.62 % 58.50/58.62 cnf(transitivity_of_success,axiom, % 58.50/58.62 ( succeeds(Goal_state,Start_state) % 58.50/58.62 | ~ succeeds(Goal_state,Intermediate_state) % 58.50/58.62 | ~ succeeds(Intermediate_state,Start_state) ) ). % 58.50/58.62 % 58.50/58.62 cnf(goto_success,axiom, % 58.50/58.62 ( succeeds(Goal_state,Start_state) % 58.50/58.62 | ~ has(Start_state,goto(Label)) % 58.50/58.62 | ~ labels(Label,Goal_state) ) ). % 58.50/58.62 % 58.50/58.62 cnf(conditional_success,axiom, % 58.50/58.62 ( succeeds(Goal_state,Start_state) % 58.50/58.62 | ~ has(Start_state,ifthen(Condition,Goal_state)) ) ). % 58.50/58.62 % 58.50/58.62 cnf(state_1,hypothesis, % 58.50/58.62 has(p1,assign(register_j,n0)) ). % 58.50/58.62 % 58.50/58.62 cnf(transition_1_to_2,hypothesis, % 58.50/58.62 follows(p2,p1) ). % 58.50/58.62 % 58.50/58.62 cnf(state_2,hypothesis, % 58.50/58.62 has(p2,assign(register_k,n1)) ). % 58.50/58.62 % 58.50/58.62 cnf(label_state_3,hypothesis, % 58.50/58.62 labels(loop,p3) ). % 58.50/58.62 % 58.50/58.62 cnf(transition_2_to_3,hypothesis, % 58.50/58.62 follows(p3,p2) ). % 58.50/58.62 % 58.50/58.62 cnf(state_3,hypothesis, % 58.50/58.62 has(p3,ifthen(equal_function(register_j,n),p4)) ). % 58.50/58.62 % 58.50/58.62 cnf(state_4,hypothesis, % 58.50/58.62 has(p4,goto(out)) ). % 58.50/58.62 % 58.50/58.62 cnf(transition_4_to_5,hypothesis, % 58.50/58.62 follows(p5,p4) ). % 58.50/58.62 % 58.50/58.62 cnf(transition_3_to_6,hypothesis, % 58.50/58.62 follows(p6,p3) ). % 58.50/58.62 % 58.50/58.62 cnf(state_6,hypothesis, % 58.50/58.62 has(p6,assign(register_k,times(n2,register_k))) ). % 58.50/58.62 % 58.50/58.62 cnf(transition_6_to_7,hypothesis, % 58.50/58.62 follows(p7,p6) ). % 58.50/58.62 % 58.50/58.62 cnf(state_7,hypothesis, % 58.50/58.62 has(p7,assign(register_j,plus(register_j,n1))) ). % 58.50/58.62 % 58.50/58.62 cnf(transition_7_to_8,hypothesis, % 58.50/58.62 follows(p8,p7) ). % 58.50/58.62 % 58.50/58.62 cnf(state_8,hypothesis, % 58.50/58.62 has(p8,goto(loop)) ). % 58.50/58.62 % 58.50/58.62 cnf(prove_there_is_a_loop_through_p3,negated_conjecture, % 58.50/58.62 ~ succeeds(p3,p3) ). % 58.50/58.62 % 58.50/58.62 %-------------------------------------------------------------------------- % 58.50/58.62 %------------------------------------------- % 58.50/58.62 % Proof found % 58.50/58.62 % SZS status Theorem for theBenchmark % 58.50/58.62 % SZS output start Proof % 58.50/58.63 %ClaNum:19(EqnAxiom:0) % 58.50/58.63 %VarNum:21(SingletonVarNum:11) % 58.50/58.63 %MaxLitNum:3 % 58.50/58.63 %MaxfuncDepth:2 % 58.50/58.63 %SharedTerms:41 % 58.50/58.63 %goalClause: 15 % 58.50/58.63 %singleGoalClaCount:1 % 58.50/58.63 [1]P1(a1,a2) % 58.50/58.63 [2]P1(a13,a1) % 58.50/58.63 [3]P1(a14,a15) % 58.50/58.63 [4]P1(a16,a13) % 58.50/58.63 [5]P1(a17,a16) % 58.50/58.63 [6]P1(a18,a17) % 58.50/58.63 [7]P2(a3,a13) % 58.50/58.63 [15]~P4(a13,a13) % 58.50/58.63 [8]P3(a15,f4(a8)) % 58.50/58.63 [9]P3(a18,f4(a3)) % 58.50/58.63 [10]P3(a2,f5(a19,a9)) % 58.50/58.63 [11]P3(a1,f5(a21,a11)) % 58.50/58.63 [12]P3(a16,f5(a21,f22(a12,a21))) % 58.50/58.63 [13]P3(a17,f5(a19,f20(a19,a11))) % 58.50/58.63 [14]P3(a13,f7(f6(a19,a10),a15)) % 58.50/58.63 [16]~P1(x161,x162)+P4(x161,x162) % 58.50/58.63 [19]P4(x191,x192)+~P3(x192,f7(x193,x191)) % 58.50/58.63 [17]~P4(x171,x173)+P4(x171,x172)+~P4(x173,x172) % 58.50/58.63 [18]P4(x181,x182)+~P2(x183,x181)+~P3(x182,f4(x183)) % 58.50/58.63 %EqnAxiom % 58.50/58.63 % 58.50/58.63 %------------------------------------------- % 58.60/58.72 cnf(30,plain, % 58.60/58.72 (P4(a13,a18)), % 58.60/58.72 inference(scs_inference,[],[15,7,9,16,18])). % 58.60/58.72 cnf(13517,plain, % 58.60/58.72 (~P4(a18,a13)), % 58.60/58.72 inference(scs_inference,[],[15,30,16,17])). % 58.60/58.72 cnf(151853,plain, % 58.60/58.72 (P4(a16,a13)), % 58.60/58.72 inference(scs_inference,[],[4,16])). % 58.60/58.72 cnf(151861,plain, % 58.60/58.72 (~P4(a18,a16)), % 58.60/58.72 inference(scs_inference,[],[151853,1,13517,16,17])). % 58.60/58.72 cnf(151877,plain, % 58.60/58.72 (P4(a17,a16)), % 58.60/58.72 inference(scs_inference,[],[5,16])). % 58.60/58.72 cnf(151885,plain, % 58.60/58.72 ($false), % 58.60/58.72 inference(scs_inference,[],[151861,151877,6,16,17]), % 58.60/58.72 ['proof']). % 58.69/58.79 % SZS output end Proof % 58.69/58.79 % Total time :58.010000s %------------------------------------------------------------------------------