%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : MSC002-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 : n001.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 11:52:10 EDT 2024 % Result : Unsatisfiable 58.59s 58.63s % Output : CNFRefutation 58.78s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : MSC002-1 : TPTP v8.2.0. Released v1.0.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n001.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 : Sat Jun 22 05:38:54 EDT 2024 % 0.12/0.33 % CPUTime : % 0.45/0.57 start to proof:theBenchmark % 58.57/58.61 %------------------------------------------- % 58.57/58.61 % File :CSE---1.7 % 58.57/58.61 % Problem :theBenchmark % 58.57/58.61 % Transform :cnf % 58.57/58.61 % Format :tptp:raw % 58.57/58.61 % Command :java -jar mcs_scs.jar %d %s % 58.57/58.61 % 58.57/58.61 % Result :Theorem 58.010000s % 58.57/58.62 % Output :CNFRefutation 58.010000s % 58.57/58.62 %------------------------------------------- % 58.59/58.63 %-------------------------------------------------------------------------- % 58.59/58.63 % File : MSC002-1 : TPTP v8.2.0. Released v1.0.0. % 58.59/58.63 % Domain : Miscellaneous % 58.59/58.63 % Problem : A Blind Hand Problem % 58.59/58.63 % Version : Especial. % 58.59/58.63 % English : % 58.59/58.63 % 58.59/58.63 % Refs : [Pop70] Popplestone (1970), Freddy, Things and Sets % 58.59/58.63 % : [MRS72] Michie et al. (1972), G-deduction % 58.59/58.63 % : [WM76] Wilson & Minker (1976), Resolution, Refinements, and S % 58.59/58.63 % Source : [SPRFN] % 58.59/58.63 % Names : DBABHP [MRS72] % 58.59/58.63 % : DBABHP [WM76] % 58.59/58.63 % 58.59/58.63 % Status : Unsatisfiable % 58.59/58.63 % Rating : 0.00 v7.1.0, 0.17 v7.0.0, 0.12 v6.3.0, 0.14 v6.2.0, 0.11 v6.1.0, 0.14 v5.5.0, 0.25 v5.4.0, 0.10 v5.1.0, 0.09 v5.0.0, 0.00 v2.0.0 % 58.59/58.63 % Syntax : Number of clauses : 14 ( 3 unt; 1 nHn; 10 RR) % 58.59/58.63 % Number of literals : 30 ( 0 equ; 17 neg) % 58.59/58.63 % Maximal clause size : 3 ( 2 avg) % 58.59/58.63 % Maximal term depth : 4 ( 1 avg) % 58.59/58.63 % Number of predicates : 7 ( 7 usr; 0 prp; 1-3 aty) % 58.59/58.63 % Number of functors : 7 ( 7 usr; 4 con; 0-2 aty) % 58.59/58.63 % Number of variables : 36 ( 8 sgn) % 58.59/58.63 % SPC : CNF_UNS_RFO_NEQ_NHN % 58.59/58.63 % 58.59/58.63 % Comments : The symbols are explained in [MRS72]. % 58.59/58.63 %-------------------------------------------------------------------------- % 58.59/58.63 cnf(something_is_here_now,axiom, % 58.59/58.63 at(something,here,now) ). % 58.59/58.63 % 58.59/58.63 cnf(hand_let_go,axiom, % 58.59/58.63 ( ~ hand_at(Place,Situation) % 58.59/58.63 | hand_at(Place,let_go(Situation)) ) ). % 58.59/58.63 % 58.59/58.63 cnf(hand_go,axiom, % 58.59/58.63 ( ~ hand_at(Place,Situation) % 58.59/58.63 | hand_at(Another_place,go(Another_place,Situation)) ) ). % 58.59/58.63 % 58.59/58.63 cnf(cant_hold_and_let_go,axiom, % 58.59/58.63 ~ held(Thing,let_go(Situation)) ). % 58.59/58.63 % 58.59/58.63 cnf(everything_is_red,axiom, % 58.59/58.63 ( ~ at(Thing,here,Situation) % 58.59/58.63 | red(Thing) ) ). % 58.59/58.63 % 58.59/58.63 cnf(situation_let_go,axiom, % 58.59/58.63 ( ~ at(Thing,Place,Situation) % 58.59/58.63 | at(Thing,Place,let_go(Situation)) ) ). % 58.59/58.63 % 58.59/58.63 cnf(situation_pick_up,axiom, % 58.59/58.63 ( ~ at(Thing,Place,Situation) % 58.59/58.63 | at(Thing,Place,pick_up(Situation)) ) ). % 58.59/58.63 % 58.59/58.63 cnf(can_grab_if_previously_let_go,axiom, % 58.59/58.63 ( ~ at(Thing,Place,Situation) % 58.59/58.63 | grabbed(Thing,pick_up(go(Place,let_go(Situation)))) ) ). % 58.59/58.63 % 58.59/58.63 cnf(answer_if_red_and_put_there,axiom, % 58.59/58.63 ( ~ red(Thing) % 58.59/58.63 | ~ put(Thing,there,Situation) % 58.59/58.63 | answer(Situation) ) ). % 58.59/58.63 % 58.59/58.63 cnf(can_put_somewhere_if_grab_and_go_there,axiom, % 58.59/58.63 ( ~ at(Thing,Place,Situation) % 58.59/58.63 | ~ grabbed(Thing,Situation) % 58.59/58.63 | put(Thing,Another_place,go(Another_place,Situation)) ) ). % 58.59/58.63 % 58.59/58.63 cnf(thing_either_held_or_went_there,axiom, % 58.59/58.63 ( held(Thing,Situation) % 58.59/58.63 | ~ at(Thing,Place,Situation) % 58.59/58.63 | at(Thing,Place,go(Another_place,Situation)) ) ). % 58.59/58.63 % 58.59/58.63 cnf(thing_goes_in_hand,axiom, % 58.59/58.63 ( ~ hand_at(One_place,Situation) % 58.59/58.63 | ~ held(Thing,Situation) % 58.59/58.63 | at(Thing,Place,go(Place,Situation)) ) ). % 58.59/58.63 % 58.59/58.63 cnf(thing_picked_up_by_hand,axiom, % 58.59/58.63 ( ~ hand_at(Place,Situation) % 58.59/58.63 | ~ at(Thing,Place,Situation) % 58.59/58.63 | held(Thing,pick_up(Situation)) ) ). % 58.59/58.63 % 58.59/58.63 cnf(prove_there_is_an_answer_situation,negated_conjecture, % 58.59/58.63 ~ answer(Situation) ). % 58.59/58.63 % 58.59/58.63 %-------------------------------------------------------------------------- % 58.59/58.63 %------------------------------------------- % 58.59/58.63 % Proof found % 58.59/58.63 % SZS status Theorem for theBenchmark % 58.59/58.63 % SZS output start Proof % 58.59/58.64 %ClaNum:14(EqnAxiom:0) % 58.59/58.64 %VarNum:70(SingletonVarNum:36) % 58.59/58.64 %MaxLitNum:3 % 58.59/58.64 %MaxfuncDepth:3 % 58.59/58.64 %SharedTerms:5 % 58.59/58.64 %goalClause: 2 % 58.59/58.64 %singleGoalClaCount:1 % 58.59/58.64 [1]P1(a1,a2,a4) % 58.59/58.64 [2]~P2(x21) % 58.59/58.64 [3]~P3(x31,f5(x32)) % 58.59/58.64 [6]P6(x61)+~P1(x61,a2,x62) % 58.59/58.64 [4]~P4(x41,x42)+P4(x41,f5(x42)) % 58.59/58.64 [5]~P4(x53,x52)+P4(x51,f3(x51,x52)) % 58.59/58.64 [10]~P1(x101,x102,x103)+P1(x101,x102,f5(x103)) % 58.59/58.64 [11]~P1(x111,x112,x113)+P1(x111,x112,f6(x113)) % 58.59/58.64 [13]~P1(x131,x132,x133)+P5(x131,f6(f3(x132,f5(x133)))) % 58.59/58.64 [7]P2(x71)+~P6(x72)+~P7(x72,a7,x71) % 58.59/58.64 [9]~P1(x91,x93,x92)+~P4(x93,x92)+P3(x91,f6(x92)) % 58.59/58.64 [8]~P3(x81,x83)+~P4(x84,x83)+P1(x81,x82,f3(x82,x83)) % 58.59/58.64 [12]~P1(x121,x123,x122)+P3(x121,x122)+P1(x121,x123,f3(x124,x122)) % 58.59/58.64 [14]~P5(x141,x143)+~P1(x141,x144,x143)+P7(x141,x142,f3(x142,x143)) % 58.59/58.64 %EqnAxiom % 58.59/58.64 % 58.59/58.64 %------------------------------------------- % 58.71/58.72 cnf(18,plain, % 58.71/58.73 (P1(a1,a2,f5(f6(a4)))), % 58.71/58.73 inference(scs_inference,[],[1,10,11])). % 58.71/58.73 cnf(22,plain, % 58.71/58.73 (~P7(a1,a7,x221)), % 58.71/58.73 inference(scs_inference,[],[2,1,7,6])). % 58.71/58.73 cnf(152992,plain, % 58.71/58.73 (P5(a1,f6(f3(a2,f5(a4))))), % 58.71/58.73 inference(scs_inference,[],[18,1,10,11,13])). % 58.71/58.73 cnf(153004,plain, % 58.71/58.73 (P1(a1,a2,f6(a4))), % 58.71/58.73 inference(scs_inference,[],[1,11])). % 58.71/58.73 cnf(153006,plain, % 58.71/58.73 (P1(a1,a2,f5(a4))), % 58.71/58.73 inference(scs_inference,[],[1,11,10])). % 58.71/58.73 cnf(153013,plain, % 58.71/58.73 (P1(a1,a2,f5(f5(a4)))), % 58.71/58.73 inference(scs_inference,[],[153006,10])). % 58.71/58.73 cnf(153017,plain, % 58.71/58.73 (P1(a1,a2,f3(x1530171,f5(a4)))), % 58.71/58.73 inference(scs_inference,[],[153004,153006,3,10,11,12])). % 58.71/58.73 cnf(153032,plain, % 58.71/58.73 ($false), % 58.71/58.73 inference(scs_inference,[],[153017,153013,152992,3,22,11,10,12,14]), % 58.71/58.73 ['proof']). % 58.78/58.80 % SZS output end Proof % 58.78/58.80 % Total time :58.010000s %------------------------------------------------------------------------------