%------------------------------------------------------------------------------ % File : Scavenger---EP-0.2 % Problem : SYN000-1 : TPTP v7.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -Xmx8192M -jar scavenger.jar -a EP %s % Computer : n100.star.cs.uiowa.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz % Memory : 32218.625MB % OS : Linux 3.10.0-693.2.2.el7.x86_64 % CPULimit : 300s % DateTime : Fri Jun 1 07:58:08 EDT 2018 % Result : Unsatisfiable 4.23s % Output : CNFRefutation 4.23s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : SYN000-1 : TPTP v7.1.0. Released v4.0.0. % 0.00/0.04 % Command : java -Xmx8192M -jar scavenger.jar -a EP %s % 0.03/0.24 % Computer : n100.star.cs.uiowa.edu % 0.03/0.24 % Model : x86_64 x86_64 % 0.03/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % 0.03/0.24 % Memory : 32218.625MB % 0.03/0.24 % OS : Linux 3.10.0-693.2.2.el7.x86_64 % 0.03/0.24 % CPULimit : 300 % 0.03/0.24 % DateTime : Fri Jun 1 01:24:28 CDT 2018 % 0.03/0.24 % CPUTime: % 4.23/2.47 hasConjecture: false % 4.23/2.47 % SZS status Unsatisfiable for Scavenger---EP-0.2_n100.star.cs.uiowa.edu_2304 % 4.23/2.47 % SZS output start CNFRefutation for Scavenger---EP-0.2_n100.star.cs.uiowa.edu_2304 % 4.23/2.47 cnf(1,axiom, % 4.23/2.47 (p h), % 4.23/2.47 inference(axiom,[status(thm)],[]). % 4.23/2.47 cnf(2,axiom, % 4.23/2.47 ~((p X)), % 4.23/2.47 inference(axiom,[status(thm)],[]). % 4.23/2.47 cnf(3,axiom, % 4.23/2.47 ~((A = B)) | ~((p A)) | (p B), % 4.23/2.47 inference(axiom,[status(thm)],[]). % 4.23/2.47 cnf(4,plain, % 4.23/2.47 ~((h = B)), % 4.23/2.47 inference(unit-propagation-resolution,[],[1,2,3]). % 4.23/2.47 cnf(5,axiom, % 4.23/2.47 (A = A), % 4.23/2.47 inference(axiom,[status(thm)],[]). % 4.23/2.47 cnf(6,axiom, % 4.23/2.47 ~((A = B)) | ~((B = C)) | (A = C), % 4.23/2.47 inference(axiom,[status(thm)],[]). % 4.23/2.47 cnf(7,plain, % 4.23/2.47 (C = C), % 4.23/2.47 inference(unit-propagation-resolution,[],[5,5,6]). % 4.23/2.47 cnf(8,plain, % 4.23/2.47 $false, % 4.23/2.47 inference(conflict,[],[4,7]). % 4.23/2.47 % SZS output end CNFRefutation for Scavenger---EP-0.2_n100.star.cs.uiowa.edu_2304 % 4.56/2.53 % Scavenger ended %------------------------------------------------------------------------------