%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : MSC002-2 : TPTP v8.2.0. Released v1.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n018.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.60s 58.85s % Output : CNFRefutation 58.91s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : MSC002-2 : TPTP v8.2.0. Released v1.0.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n018.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Sat Jun 22 05:39:38 EDT 2024 % 0.13/0.34 % CPUTime : % 0.55/0.60 start to proof:theBenchmark % 58.60/58.83 %------------------------------------------- % 58.60/58.83 % File :CSE---1.7 % 58.60/58.83 % Problem :theBenchmark % 58.60/58.83 % Transform :cnf % 58.60/58.83 % Format :tptp:raw % 58.60/58.83 % Command :java -jar mcs_scs.jar %d %s % 58.60/58.83 % 58.60/58.83 % Result :Theorem 58.000000s % 58.60/58.83 % Output :CNFRefutation 58.000000s % 58.60/58.83 %------------------------------------------- % 58.60/58.84 %-------------------------------------------------------------------------- % 58.60/58.84 % File : MSC002-2 : TPTP v8.2.0. Released v1.0.0. % 58.60/58.84 % Domain : Miscellaneous % 58.60/58.84 % Problem : A Blind Hand Problem % 58.60/58.84 % Version : Especial. % 58.60/58.84 % Theorem formulation : Without hand movement. % 58.60/58.84 % English : % 58.60/58.84 % 58.60/58.84 % Refs : [Pop70] Popplestone (1970), Freddy, Things and Sets % 58.60/58.84 % : [MRS72] Michie et al. (1972), G-deduction % 58.60/58.84 % Source : [TPTP] % 58.60/58.84 % Names : % 58.60/58.84 % 58.60/58.84 % Status : Unsatisfiable % 58.60/58.84 % 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.12 v5.4.0, 0.10 v5.1.0, 0.09 v5.0.0, 0.00 v2.0.0 % 58.60/58.84 % Syntax : Number of clauses : 10 ( 3 unt; 1 nHn; 8 RR) % 58.60/58.84 % Number of literals : 20 ( 0 equ; 11 neg) % 58.60/58.84 % Maximal clause size : 3 ( 2 avg) % 58.60/58.84 % Maximal term depth : 4 ( 1 avg) % 58.60/58.84 % Number of predicates : 6 ( 6 usr; 0 prp; 1-3 aty) % 58.60/58.84 % Number of functors : 7 ( 7 usr; 4 con; 0-2 aty) % 58.60/58.84 % Number of variables : 24 ( 6 sgn) % 58.60/58.84 % SPC : CNF_UNS_RFO_NEQ_NHN % 58.60/58.84 % 58.60/58.84 % Comments : Clauses about hand movement have been removed. % 58.60/58.84 %-------------------------------------------------------------------------- % 58.60/58.84 cnf(something_is_here_now,axiom, % 58.60/58.84 at(something,here,now) ). % 58.60/58.84 % 58.60/58.84 cnf(cant_hold_and_let_go,axiom, % 58.60/58.84 ~ held(Thing,let_go(Situation)) ). % 58.60/58.84 % 58.60/58.84 cnf(everything_is_red,axiom, % 58.60/58.84 ( ~ at(Thing,here,Situation) % 58.60/58.84 | red(Thing) ) ). % 58.60/58.84 % 58.60/58.84 cnf(situation_let_go,axiom, % 58.60/58.84 ( ~ at(Thing,Place,Situation) % 58.60/58.84 | at(Thing,Place,let_go(Situation)) ) ). % 58.60/58.84 % 58.60/58.84 cnf(situation_pick_up,axiom, % 58.60/58.84 ( ~ at(Thing,Place,Situation) % 58.60/58.84 | at(Thing,Place,pick_up(Situation)) ) ). % 58.60/58.84 % 58.60/58.84 cnf(can_grab_if_previously_let_go,axiom, % 58.60/58.84 ( ~ at(Thing,Place,Situation) % 58.60/58.84 | grabbed(Thing,pick_up(go(Place,let_go(Situation)))) ) ). % 58.60/58.84 % 58.60/58.84 cnf(answer_if_red_and_put_there,axiom, % 58.60/58.84 ( ~ red(Thing) % 58.60/58.84 | ~ put(Thing,there,Situation) % 58.60/58.84 | answer(Situation) ) ). % 58.60/58.84 % 58.60/58.84 cnf(can_put_somewhere_if_grab_and_go_there,axiom, % 58.60/58.84 ( ~ at(Thing,Place,Situation) % 58.60/58.84 | ~ grabbed(Thing,Situation) % 58.60/58.84 | put(Thing,Another_place,go(Another_place,Situation)) ) ). % 58.60/58.84 % 58.60/58.84 cnf(thing_either_held_or_went_there,axiom, % 58.60/58.85 ( held(Thing,Situation) % 58.60/58.85 | ~ at(Thing,Place,Situation) % 58.60/58.85 | at(Thing,Place,go(Another_place,Situation)) ) ). % 58.60/58.85 % 58.60/58.85 cnf(prove_there_is_an_answer_situation,negated_conjecture, % 58.60/58.85 ~ answer(Situation) ). % 58.60/58.85 % 58.60/58.85 %-------------------------------------------------------------------------- % 58.60/58.85 %------------------------------------------- % 58.60/58.85 % Proof found % 58.60/58.85 % SZS status Theorem for theBenchmark % 58.60/58.85 % SZS output start Proof % 58.60/58.85 %ClaNum:10(EqnAxiom:0) % 58.60/58.85 %VarNum:46(SingletonVarNum:24) % 58.60/58.85 %MaxLitNum:3 % 58.60/58.85 %MaxfuncDepth:3 % 58.60/58.85 %SharedTerms:5 % 58.60/58.85 %goalClause: 2 % 58.60/58.85 %singleGoalClaCount:1 % 58.60/58.85 [1]P1(a1,a2,a4) % 58.60/58.85 [2]~P2(x21) % 58.60/58.85 [3]~P3(x31,f5(x32)) % 58.60/58.85 [4]P5(x41)+~P1(x41,a2,x42) % 58.60/58.85 [6]~P1(x61,x62,x63)+P1(x61,x62,f5(x63)) % 58.60/58.85 [7]~P1(x71,x72,x73)+P1(x71,x72,f6(x73)) % 58.60/58.85 [9]~P1(x91,x92,x93)+P4(x91,f6(f3(x92,f5(x93)))) % 58.60/58.85 [5]P2(x51)+~P5(x52)+~P6(x52,a7,x51) % 58.60/58.86 [8]~P1(x81,x83,x82)+P3(x81,x82)+P1(x81,x83,f3(x84,x82)) % 58.60/58.86 [10]~P4(x101,x103)+~P1(x101,x104,x103)+P6(x101,x102,f3(x102,x103)) % 58.60/58.86 %EqnAxiom % 58.60/58.86 % 58.60/58.86 %------------------------------------------- % 58.80/59.01 cnf(13,plain, % 58.80/59.01 (P1(a1,a2,f5(f6(a4)))), % 58.80/59.01 inference(scs_inference,[],[1,6,7])). % 58.80/59.01 cnf(15,plain, % 58.80/59.01 (~P6(a1,a7,x151)), % 58.80/59.01 inference(scs_inference,[],[2,1,5,4])). % 58.80/59.01 cnf(19,plain, % 58.80/59.01 (P1(a1,a2,f3(x191,f5(a4)))), % 58.80/59.01 inference(scs_inference,[],[3,1,8,6])). % 58.80/59.01 cnf(269732,plain, % 58.80/59.01 (~P1(a1,x2697321,f6(f3(a2,f5(a4))))), % 58.80/59.01 inference(scs_inference,[],[3,13,15,1,6,7,9,8,10])). % 58.80/59.01 cnf(269770,plain, % 58.80/59.01 ($false), % 58.80/59.01 inference(scs_inference,[],[269732,19,6,7]), % 58.80/59.01 ['proof']). % 58.91/59.13 % SZS output end Proof % 58.91/59.13 % Total time :58.000000s %------------------------------------------------------------------------------