%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : COM002-2 : 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 : n027.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.63s 59.14s % Output : CNFRefutation 59.24s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : COM002-2 : 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.11/0.33 % Computer : n027.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 300 % 0.11/0.33 % DateTime : Fri Jun 21 00:10:54 EDT 2024 % 0.11/0.33 % CPUTime : % 0.50/0.59 start to proof:theBenchmark % 58.63/59.11 %------------------------------------------- % 58.63/59.11 % File :CSE---1.7 % 58.63/59.11 % Problem :theBenchmark % 58.63/59.11 % Transform :cnf % 58.63/59.11 % Format :tptp:raw % 58.63/59.11 % Command :java -jar mcs_scs.jar %d %s % 58.63/59.11 % 58.63/59.11 % Result :Theorem 58.000000s % 58.63/59.11 % Output :CNFRefutation 58.000000s % 58.63/59.11 %------------------------------------------- % 58.63/59.13 %-------------------------------------------------------------------------- % 58.63/59.13 % File : COM002-2 : TPTP v8.2.0. Released v1.0.0. % 58.63/59.13 % Domain : Computing Theory % 58.63/59.13 % Problem : A program correctness theorem. % 58.63/59.13 % Version : Especial. % 58.63/59.13 % Theorem formulation : Considers failure rather than success % 58.63/59.13 % in the state space. % 58.63/59.13 % English : A computing state space, with eight states - P1 to P8. % 58.63/59.13 % P1 leads to P3 via P2. There is a branch at P3 such that the % 58.63/59.13 % following state is either P4 or P6. P6 leads to P8, which has % 58.63/59.13 % a loop back to P3, while P4 leads to termination. The problem % 58.63/59.13 % is to show that there is a loop in the computation, passing % 58.63/59.13 % through P3. % 58.63/59.13 % 58.63/59.13 % Refs : [RR+72] Reboh et al. (1972), Study of automatic theorem provin % 58.63/59.13 % Source : [TPTP] % 58.63/59.13 % Names : % 58.63/59.13 % 58.63/59.13 % Status : Unsatisfiable % 58.63/59.13 % Rating : 0.00 v2.1.0, 0.12 v2.0.0 % 58.63/59.13 % Syntax : Number of clauses : 19 ( 15 unt; 1 nHn; 18 RR) % 58.63/59.13 % Number of literals : 25 ( 0 equ; 8 neg) % 58.63/59.13 % Maximal clause size : 3 ( 1 avg) % 58.63/59.13 % Maximal term depth : 3 ( 1 avg) % 58.63/59.13 % Number of predicates : 4 ( 4 usr; 0 prp; 2-2 aty) % 58.63/59.13 % Number of functors : 22 ( 22 usr; 16 con; 0-2 aty) % 58.63/59.13 % Number of variables : 11 ( 1 sgn) % 58.63/59.13 % SPC : CNF_UNS_RFO_NEQ_NHN % 58.63/59.13 % 58.63/59.13 % Comments : I suspect this problem was originally by R.M. Burstall. % 58.63/59.13 %-------------------------------------------------------------------------- % 58.63/59.13 cnf(direct_success,axiom, % 58.63/59.13 ( ~ fails(Goal_state,Start_state) % 58.63/59.13 | ~ follows(Goal_state,Start_state) ) ). % 58.63/59.13 % 58.63/59.13 cnf(transitivity_of_success,axiom, % 58.63/59.13 ( ~ fails(Goal_state,Start_state) % 58.63/59.13 | fails(Goal_state,Intermediate_state) % 58.63/59.13 | fails(Intermediate_state,Start_state) ) ). % 58.63/59.13 % 58.63/59.13 cnf(goto_success,axiom, % 58.63/59.13 ( ~ fails(Goal_state,Start_state) % 58.63/59.13 | ~ has(Start_state,goto(Label)) % 58.63/59.13 | ~ labels(Label,Goal_state) ) ). % 58.63/59.13 % 58.63/59.13 cnf(conditional_success,axiom, % 58.63/59.13 ( ~ fails(Goal_state,Start_state) % 58.63/59.13 | ~ has(Start_state,ifthen(Condition,Goal_state)) ) ). % 58.63/59.13 % 58.63/59.13 cnf(state_1,hypothesis, % 58.63/59.13 has(p1,assign(register_j,n0)) ). % 58.63/59.13 % 58.63/59.13 cnf(transition_1_to_2,hypothesis, % 58.63/59.13 follows(p2,p1) ). % 58.63/59.13 % 58.63/59.13 cnf(state_2,hypothesis, % 58.63/59.13 has(p2,assign(register_k,n1)) ). % 58.63/59.13 % 58.63/59.13 cnf(label_state_3,hypothesis, % 58.63/59.13 labels(loop,p3) ). % 58.63/59.13 % 58.63/59.13 cnf(transition_2_to_3,hypothesis, % 58.63/59.13 follows(p3,p2) ). % 58.63/59.13 % 58.63/59.13 cnf(state_3,hypothesis, % 58.63/59.13 has(p3,ifthen(equal_function(register_j,n),p4)) ). % 58.63/59.13 % 58.63/59.13 cnf(state_4,hypothesis, % 58.63/59.13 has(p4,goto(out)) ). % 58.63/59.13 % 58.63/59.13 cnf(transition_4_to_5,hypothesis, % 58.63/59.13 follows(p5,p4) ). % 58.63/59.13 % 58.63/59.13 cnf(transition_3_to_6,hypothesis, % 58.63/59.13 follows(p6,p3) ). % 58.63/59.13 % 58.63/59.13 cnf(state_6,hypothesis, % 58.63/59.13 has(p6,assign(register_k,times(n2,register_k))) ). % 58.63/59.13 % 58.63/59.13 cnf(transition_6_to_7,hypothesis, % 58.63/59.13 follows(p7,p6) ). % 58.63/59.13 % 58.63/59.13 cnf(state_7,hypothesis, % 58.63/59.13 has(p7,assign(register_j,plus(register_j,n1))) ). % 58.63/59.13 % 58.63/59.13 cnf(transition_7_to_8,hypothesis, % 58.63/59.13 follows(p8,p7) ). % 58.63/59.14 % 58.63/59.14 cnf(state_8,hypothesis, % 58.63/59.14 has(p8,goto(loop)) ). % 58.63/59.14 % 58.63/59.14 cnf(prove_there_is_a_loop_through_p3,negated_conjecture, % 58.63/59.14 fails(p3,p3) ). % 58.63/59.14 % 58.63/59.14 %-------------------------------------------------------------------------- % 58.63/59.14 %------------------------------------------- % 58.63/59.14 % Proof found % 58.63/59.14 % SZS status Theorem for theBenchmark % 58.63/59.14 % SZS output start Proof % 58.63/59.15 %ClaNum:19(EqnAxiom:0) % 58.63/59.15 %VarNum:21(SingletonVarNum:11) % 58.63/59.15 %MaxLitNum:3 % 58.63/59.15 %MaxfuncDepth:2 % 58.63/59.15 %SharedTerms:41 % 58.63/59.15 %goalClause: 1 % 58.63/59.15 %singleGoalClaCount:1 % 58.63/59.15 [1]P1(a1,a1) % 58.63/59.15 [2]P2(a2,a3) % 58.63/59.15 [3]P2(a1,a2) % 58.63/59.15 [4]P2(a14,a15) % 58.63/59.15 [5]P2(a16,a1) % 58.63/59.15 [6]P2(a17,a16) % 58.63/59.15 [7]P2(a18,a17) % 58.63/59.15 [8]P3(a4,a1) % 58.63/59.15 [9]P4(a15,f5(a9)) % 58.63/59.15 [10]P4(a18,f5(a4)) % 58.63/59.15 [11]P4(a3,f6(a19,a10)) % 58.63/59.15 [12]P4(a2,f6(a21,a12)) % 58.63/59.15 [13]P4(a16,f6(a21,f22(a13,a21))) % 58.63/59.15 [14]P4(a17,f6(a19,f20(a19,a12))) % 58.63/59.15 [15]P4(a1,f8(f7(a19,a11),a15)) % 58.63/59.15 [16]~P2(x161,x162)+~P1(x161,x162) % 58.63/59.15 [19]~P1(x191,x192)+~P4(x192,f8(x193,x191)) % 58.63/59.15 [17]~P1(x173,x172)+P1(x171,x172)+P1(x173,x171) % 58.63/59.15 [18]~P1(x181,x182)+~P3(x183,x181)+~P4(x182,f5(x183)) % 58.63/59.15 %EqnAxiom % 58.63/59.15 % 58.63/59.15 %------------------------------------------- % 58.98/59.47 cnf(24,plain, % 58.98/59.47 (~P1(a1,a18)), % 58.98/59.47 inference(scs_inference,[],[1,8,10,15,16,19,18])). % 58.98/59.47 cnf(30,plain, % 58.98/59.47 (P1(a18,a1)), % 58.98/59.47 inference(scs_inference,[],[1,24,16,17])). % 58.98/59.47 cnf(572066,plain, % 58.98/59.47 (~P1(a16,a1)), % 58.98/59.47 inference(scs_inference,[],[5,16])). % 58.98/59.47 cnf(572078,plain, % 58.98/59.47 (~P1(a17,a16)), % 58.98/59.47 inference(scs_inference,[],[6,16])). % 58.98/59.47 cnf(572080,plain, % 58.98/59.47 (P1(a18,a16)), % 58.98/59.47 inference(scs_inference,[],[6,572066,30,16,17])). % 58.98/59.47 cnf(572084,plain, % 58.98/59.47 (~P1(a18,a17)), % 58.98/59.47 inference(scs_inference,[],[7,16])). % 58.98/59.47 cnf(572100,plain, % 58.98/59.47 ($false), % 58.98/59.47 inference(scs_inference,[],[572084,572080,572078,17]), % 58.98/59.47 ['proof']). % 59.24/59.73 % SZS output end Proof % 59.24/59.73 % Total time :58.000000s %------------------------------------------------------------------------------