%------------------------------------------------------------------------------ % File : Scavenger---EP-0.2 % Problem : PHI011+1 : TPTP v7.2.0. Released v7.2.0. % Transfm : none % Format : tptp:raw % Command : java -Xmx8192M -jar scavenger.jar -a EP %s % Computer : n074.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 : Tue May 29 12:48:19 EDT 2018 % Result : Theorem 30.97s % Output : CNFRefutation 30.97s % 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 : PHI011+1 : TPTP v7.2.0. Released v7.2.0. % 0.00/0.04 % Command : java -Xmx8192M -jar scavenger.jar -a EP %s % 0.03/0.24 % Computer : n074.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 : Tue May 29 11:08:29 CDT 2018 % 0.03/0.24 % CPUTime : % 6.29/3.10 11:08:32.179 INFO prover - Equality reasoning problem % 6.29/3.10 SLF4J: A number (4) of logging calls during the initialization phase have been intercepted and are % 6.29/3.10 SLF4J: now being replayed. These are subject to the filtering rules of the underlying logging system. % 6.29/3.10 SLF4J: See also http://www.slf4j.org/codes.html#replay % 6.29/3.10 11:08:32.182 INFO prover - Equality reasoning problem % 30.97/12.37 hasConjecture: true % 30.97/12.37 % SZS status Theorem for Scavenger---EP-0.2_n074.star.cs.uiowa.edu_6130 % 30.97/12.37 % SZS output start CNFRefutation for Scavenger---EP-0.2_n074.star.cs.uiowa.edu_6130 % 30.97/12.37 cnf(1,axiom, % 30.97/12.37 (property skolemize0), % 30.97/12.37 inference(axiom,[status(thm)],[]). % 30.97/12.37 cnf(2,plain, % 30.97/12.37 (predicate3 X_5 X_6 X_7 X_5 X_6 X_7), % 30.97/12.37 inference(decision,[],[]). % 30.97/12.37 cnf(3,axiom, % 30.97/12.37 (A = A), % 30.97/12.37 inference(axiom,[status(thm)],[]). % 30.97/12.37 cnf(4,axiom, % 30.97/12.37 ~((A = G)) | ~((B = H)) | ~((C = I)) | ~((D = J)) | ~((E = K)) | ~((F = L)) | ~((predicate3 A B C D E F)) | (predicate3 G H I J K L), % 30.97/12.37 inference(axiom,[status(thm)],[]). % 30.97/12.37 cnf(5,plain, % 30.97/12.37 (predicate3 G H I G H I), % 30.97/12.37 inference(unit-propagation-resolution,[],[2,3,3,3,3,3,3,4]). % 30.97/12.37 cnf(6,axiom, % 30.97/12.37 (is_the skolemize2 skolemize0), % 30.97/12.37 inference(axiom,[status(thm)],[]). % 30.97/12.37 cnf(7,axiom, % 30.97/12.37 ~((exemplifies_property skolemize0 skolemize2)), % 30.97/12.37 inference(axiom,[status(thm)],[]). % 30.97/12.37 cnf(8,axiom, % 30.97/12.37 ~((predicate6 X_5 X_6 X_7 X_6 X_7)) | ~((predicate3 X_5 X_6 X_7 X_5 X_6 X_7)) | (exemplifies_property X_6 X_7), % 30.97/12.37 inference(axiom,[status(thm)],[]). % 30.97/12.37 cnf(9,plain, % 30.97/12.37 ~((predicate6 X_5 skolemize0 skolemize2 skolemize0 skolemize2)), % 30.97/12.37 inference(unit-propagation-resolution,[],[2,7,8]). % 30.97/12.37 cnf(10,axiom, % 30.97/12.37 ~((is_the X_5 X_6)) | ~((predicate3 X_5 X_6 X_7 X_5 X_6 X_7)) | (predicate6 X_5 X_6 X_7 X_6 X_7) | (predicate7 X_5 X_6 X_5 X_7), % 30.97/12.37 inference(axiom,[status(thm)],[]). % 30.97/12.37 cnf(11,plain, % 30.97/12.37 (predicate7 skolemize2 skolemize0 skolemize2 skolemize2), % 30.97/12.37 inference(unit-propagation-resolution,[],[5,6,9,10]). % 30.97/12.37 cnf(12,axiom, % 30.97/12.37 ~((X_5 = X_7)) | ~((predicate7 X_5 X_6 X_5 X_7)) | ~((predicate3 X_5 X_6 X_7 X_5 X_6 X_7)) | (predicate6 X_5 X_6 X_7 X_6 X_7), % 30.97/12.37 inference(axiom,[status(thm)],[]). % 30.97/12.37 cnf(13,plain, % 30.97/12.37 ~((predicate7 skolemize2 skolemize0 skolemize2 skolemize2)), % 30.97/12.37 inference(unit-propagation-resolution,[],[5,3,9,12]). % 30.97/12.37 cnf(14,plain, % 30.97/12.37 $false, % 30.97/12.37 inference(conflict,[],[11,13]). % 30.97/12.37 cnf(15,plain, % 30.97/12.37 ~((predicate3 skolemize2 skolemize0 skolemize2 skolemize2 skolemize0 skolemize2)), % 30.97/12.37 inference(conflict-driven-clause-learning,[],[14]). % 30.97/12.37 cnf(16,axiom, % 30.97/12.37 (object skolemize2), % 30.97/12.37 inference(axiom,[status(thm)],[]). % 30.97/12.37 cnf(17,plain, % 30.97/12.37 $false, % 30.97/12.37 inference(conflict,[],[11,13]). % 30.97/12.37 cnf(18,plain, % 30.97/12.37 ~((predicate3 skolemize2 skolemize0 skolemize2 skolemize2 skolemize0 skolemize2)), % 30.97/12.37 inference(conflict-driven-clause-learning,[],[17]). % 30.97/12.37 cnf(19,axiom, % 30.97/12.37 ~((object X_7)) | ~((predicate4 X_5 X_6 X_7)) | (predicate3 X_5 X_6 X_7 X_5 X_6 X_7), % 30.97/12.37 inference(axiom,[status(thm)],[]). % 30.97/12.37 cnf(20,plain, % 30.97/12.37 ~((predicate4 skolemize2 skolemize0 skolemize2)), % 30.97/12.37 inference(unit-propagation-resolution,[],[16,18,19]). % 30.97/12.37 cnf(21,axiom, % 30.97/12.37 ~((property X_6)) | ~((predicate5 X_5 X_6)) | (predicate3 X_5 X_6 X_7 X_5 X_6 X_7) | (predicate4 X_5 X_6 X_7), % 30.97/12.37 inference(axiom,[status(thm)],[]). % 30.97/12.37 cnf(22,plain, % 30.97/12.37 ~((predicate5 skolemize2 skolemize0)), % 30.97/12.37 inference(unit-propagation-resolution,[],[1,15,20,21]). % 30.97/12.37 cnf(23,axiom, % 30.97/12.37 ~((object X_5)) | (predicate3 X_5 X_6 X_7 X_5 X_6 X_7) | (predicate4 X_5 X_6 X_7) | (predicate5 X_5 X_6), % 30.97/12.37 inference(axiom,[status(thm)],[]). % 30.97/12.37 cnf(24,plain, % 30.97/12.37 (predicate5 skolemize2 skolemize0), % 30.97/12.37 inference(unit-propagation-resolution,[],[16,15,20,23]). % 30.97/12.37 cnf(25,plain, % 30.97/12.37 $false, % 30.97/12.37 inference(conflict,[],[22,24]). % 30.97/12.37 % SZS output end CNFRefutation for Scavenger---EP-0.2_n074.star.cs.uiowa.edu_6130 % 31.01/12.40 % Scavenger ended %------------------------------------------------------------------------------