%------------------------------------------------------------------------------ % File : Scavenger---EP-0.2 % Problem : PHI014+1 : TPTP v7.2.0. Released v7.2.0. % Transfm : none % Format : tptp:raw % Command : java -Xmx8192M -jar scavenger.jar -a EP %s % Computer : n077.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:20 EDT 2018 % Result : Theorem 6.84s % Output : CNFRefutation 6.84s % 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 : PHI014+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 : n077.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:09:44 CDT 2018 % 0.03/0.24 % CPUTime : % 6.03/3.05 SLF4J: A number (35) of logging calls during the initialization phase have been intercepted and are % 6.03/3.05 SLF4J: now being replayed. These are subject to the filtering rules of the underlying logging system. % 6.03/3.05 SLF4J: See also http://www.slf4j.org/codes.html#replay % 6.84/3.30 hasConjecture: true % 6.84/3.30 % SZS status Theorem for Scavenger---EP-0.2_n077.star.cs.uiowa.edu_30326 % 6.84/3.31 % SZS output start CNFRefutation for Scavenger---EP-0.2_n077.star.cs.uiowa.edu_30326 % 6.84/3.31 cnf(1,axiom, % 6.84/3.31 (is_the god none_greater), % 6.84/3.31 inference(axiom,[status(thm)],[]). % 6.84/3.31 cnf(2,axiom, % 6.84/3.31 ~((is_the X_3 X_4)) | (predicate5 X_3 X_4 X_4 X_3), % 6.84/3.31 inference(axiom,[status(thm)],[]). % 6.84/3.31 cnf(3,plain, % 6.84/3.31 (predicate5 god none_greater none_greater god), % 6.84/3.31 inference(unit-propagation-resolution,[],[1,2]). % 6.84/3.31 cnf(4,axiom, % 6.84/3.31 ~((predicate5 X_3 X_4 X_4 X_3)) | (object X_3), % 6.84/3.31 inference(axiom,[status(thm)],[]). % 6.84/3.31 cnf(5,plain, % 6.84/3.31 (object god), % 6.84/3.31 inference(unit-propagation-resolution,[],[3,4]). % 6.84/3.31 cnf(6,axiom, % 6.84/3.31 ~((object X_5)) | (predicate6 X_5 X_5 X_6), % 6.84/3.31 inference(axiom,[status(thm)],[]). % 6.84/3.31 cnf(7,plain, % 6.84/3.31 (predicate6 god god X_6), % 6.84/3.31 inference(unit-propagation-resolution,[],[5,6]). % 6.84/3.31 cnf(8,axiom, % 6.84/3.31 ~((predicate5 X_3 X_4 X_4 X_3)) | (property X_4), % 6.84/3.31 inference(axiom,[status(thm)],[]). % 6.84/3.31 cnf(9,plain, % 6.84/3.31 (property none_greater), % 6.84/3.31 inference(unit-propagation-resolution,[],[3,8]). % 6.84/3.31 cnf(10,axiom, % 6.84/3.31 ~((property X_0)) | (predicate0 X_0 X_1 X_0 X_2), % 6.84/3.31 inference(axiom,[status(thm)],[]). % 6.84/3.31 cnf(11,plain, % 6.84/3.31 (predicate0 none_greater X_1 none_greater X_2), % 6.84/3.31 inference(unit-propagation-resolution,[],[9,10]). % 6.84/3.31 cnf(12,plain, % 6.84/3.31 ~((predicate1 X_1 X_0 X_2 X_0)), % 6.84/3.31 inference(decision,[],[]). % 6.84/3.31 cnf(13,axiom, % 6.84/3.31 ~((is_the X_1 X_0)) | ~((predicate2 X_1 X_1 X_0)) | ~((predicate0 X_0 X_1 X_0 X_2)) | (predicate1 X_1 X_0 X_2 X_0), % 6.84/3.31 inference(axiom,[status(thm)],[]). % 6.84/3.31 cnf(14,plain, % 6.84/3.31 ~((predicate2 god god none_greater)), % 6.84/3.31 inference(unit-propagation-resolution,[],[11,1,12,13]). % 6.84/3.31 cnf(15,axiom, % 6.84/3.31 ~((object X_1)) | ~((predicate0 X_0 X_1 X_0 X_2)) | (predicate1 X_1 X_0 X_2 X_0) | (predicate2 X_1 X_1 X_0), % 6.84/3.31 inference(axiom,[status(thm)],[]). % 6.84/3.31 cnf(16,plain, % 6.84/3.31 (predicate2 god god none_greater), % 6.84/3.31 inference(unit-propagation-resolution,[],[11,5,12,15]). % 6.84/3.31 cnf(17,plain, % 6.84/3.31 $false, % 6.84/3.31 inference(conflict,[],[14,16]). % 6.84/3.31 cnf(18,plain, % 6.84/3.31 (predicate1 god none_greater X_2 none_greater), % 6.84/3.31 inference(conflict-driven-clause-learning,[],[17]). % 6.84/3.31 cnf(19,axiom, % 6.84/3.31 ~((object X_2)) | ~((predicate1 X_1 X_0 X_2 X_0)) | ~((predicate0 X_0 X_1 X_0 X_2)) | (predicate3 X_2 X_2 X_0), % 6.84/3.31 inference(axiom,[status(thm)],[]). % 6.84/3.31 cnf(20,plain, % 6.84/3.31 (predicate3 god god none_greater), % 6.84/3.31 inference(unit-propagation-resolution,[],[11,18,5,19]). % 6.84/3.31 cnf(21,plain, % 6.84/3.31 $false, % 6.84/3.31 inference(conflict,[],[14,16]). % 6.84/3.31 cnf(22,plain, % 6.84/3.31 (predicate1 god none_greater X_2 none_greater), % 6.84/3.31 inference(conflict-driven-clause-learning,[],[21]). % 6.84/3.31 cnf(23,axiom, % 6.84/3.31 ~((is_the X_2 X_0)) | ~((predicate3 X_2 X_2 X_0)) | ~((predicate1 X_1 X_0 X_2 X_0)) | ~((predicate0 X_0 X_1 X_0 X_2)) | (predicate4 X_2 X_0 X_0 X_2), % 6.84/3.31 inference(axiom,[status(thm)],[]). % 6.84/3.31 cnf(24,plain, % 6.84/3.31 (predicate4 god none_greater none_greater god), % 6.84/3.31 inference(unit-propagation-resolution,[],[11,22,20,1,23]). % 6.84/3.31 cnf(25,axiom, % 6.84/3.31 ~((predicate4 X_2 X_0 X_0 X_2)) | ~((predicate3 X_2 X_2 X_0)) | ~((predicate1 X_1 X_0 X_2 X_0)) | ~((predicate0 X_0 X_1 X_0 X_2)) | (exemplifies_property X_0 X_2), % 6.84/3.31 inference(axiom,[status(thm)],[]). % 6.84/3.31 cnf(26,plain, % 6.84/3.31 (exemplifies_property none_greater god), % 6.84/3.31 inference(unit-propagation-resolution,[],[11,18,20,24,25]). % 6.84/3.31 cnf(27,axiom, % 6.84/3.31 ~((exemplifies_property none_greater X_5)) | ~((predicate6 X_5 X_5 X_6)) | (predicate7 X_5 X_5 X_6), % 6.84/3.31 inference(axiom,[status(thm)],[]). % 6.84/3.31 cnf(28,plain, % 6.84/3.31 (predicate7 god god X_6), % 6.84/3.31 inference(unit-propagation-resolution,[],[7,26,27]). % 6.84/3.31 cnf(29,axiom, % 6.84/3.31 ~((object X_7)) | (predicate12 X_7 X_7), % 6.84/3.31 inference(axiom,[status(thm)],[]). % 6.84/3.31 cnf(30,plain, % 6.84/3.31 (predicate12 god god), % 6.84/3.31 inference(unit-propagation-resolution,[],[5,29]). % 6.84/3.31 cnf(31,plain, % 6.84/3.31 ~((predicate14 X_7 X_7)), % 6.84/3.31 inference(decision,[],[]). % 6.84/3.31 cnf(32,axiom, % 6.84/3.31 ~((is_the X_7 none_greater)) | ~((predicate12 X_7 X_7)) | (predicate13 X_7 X_7) | (predicate14 X_7 X_7), % 6.84/3.31 inference(axiom,[status(thm)],[]). % 6.84/3.31 cnf(33,plain, % 6.84/3.31 (predicate13 god god), % 6.84/3.31 inference(unit-propagation-resolution,[],[30,1,31,32]). % 6.84/3.31 cnf(34,axiom, % 6.84/3.31 ~((predicate13 X_7 X_7)) | ~((predicate12 X_7 X_7)) | (object (skolemize1 X_7)), % 6.84/3.31 inference(axiom,[status(thm)],[]). % 6.84/3.31 cnf(35,plain, % 6.84/3.31 (object (skolemize1 god)), % 6.84/3.31 inference(unit-propagation-resolution,[],[30,33,34]). % 6.84/3.31 cnf(36,plain, % 6.84/3.31 ~((object X_1)), % 6.84/3.31 inference(decision,[],[]). % 6.84/3.31 cnf(37,plain, % 6.84/3.31 ~((predicate5 X_3 X_4 X_4 X_3)), % 6.84/3.31 inference(unit-propagation-resolution,[],[36,4]). % 6.84/3.31 cnf(38,plain, % 6.84/3.31 $false, % 6.84/3.31 inference(conflict,[],[3,37]). % 6.84/3.31 cnf(39,plain, % 6.84/3.31 (object god), % 6.84/3.31 inference(conflict-driven-clause-learning,[],[38]). % 6.84/3.31 cnf(40,plain, % 6.84/3.31 (object X_3), % 6.84/3.31 inference(decision,[],[]). % 6.84/3.31 cnf(41,plain, % 6.84/3.31 (predicate12 X_7 X_7), % 6.84/3.31 inference(unit-propagation-resolution,[],[40,29]). % 6.84/3.31 cnf(42,plain, % 6.84/3.31 ~((exemplifies_property conceivable X_6)), % 6.84/3.31 inference(decision,[],[]). % 6.84/3.31 cnf(43,axiom, % 6.84/3.31 ~((predicate13 X_7 X_7)) | ~((predicate12 X_7 X_7)) | (exemplifies_property conceivable (skolemize1 X_7)), % 6.84/3.31 inference(axiom,[status(thm)],[]). % 6.84/3.31 cnf(44,plain, % 6.84/3.31 ~((predicate13 god god)), % 6.84/3.31 inference(unit-propagation-resolution,[],[30,42,43]). % 6.84/3.31 cnf(45,axiom, % 6.84/3.31 ~((exemplifies_property existence god)), % 6.84/3.31 inference(axiom,[status(thm)],[]). % 6.84/3.31 cnf(46,axiom, % 6.84/3.31 ~((predicate14 X_7 X_7)) | ~((predicate12 X_7 X_7)) | (predicate13 X_7 X_7) | (exemplifies_property existence X_7), % 6.84/3.31 inference(axiom,[status(thm)],[]). % 6.84/3.31 cnf(47,plain, % 6.84/3.31 ~((predicate14 god god)), % 6.84/3.31 inference(unit-propagation-resolution,[],[41,44,45,46]). % 6.84/3.31 cnf(48,plain, % 6.84/3.31 (predicate14 god god), % 6.84/3.31 inference(unit-propagation-resolution,[],[41,1,44,32]). % 6.84/3.31 cnf(49,plain, % 6.84/3.31 $false, % 6.84/3.31 inference(conflict,[],[47,48]). % 6.84/3.31 cnf(50,plain, % 6.84/3.31 ~((object god)) | (exemplifies_property conceivable (skolemize1 god)), % 6.84/3.31 inference(conflict-driven-clause-learning,[],[49]). % 6.84/3.31 cnf(51,plain, % 6.84/3.31 (exemplifies_property conceivable (skolemize1 god)), % 6.84/3.31 inference(unit-propagation-resolution,[],[39,50]). % 6.84/3.31 cnf(52,axiom, % 6.84/3.31 ~((exemplifies_property conceivable X_6)) | ~((predicate8 X_6 X_5 X_6)) | ~((predicate7 X_5 X_5 X_6)) | ~((predicate6 X_5 X_5 X_6)), % 6.84/3.31 inference(axiom,[status(thm)],[]). % 6.84/3.31 cnf(53,plain, % 6.84/3.31 ~((predicate8 (skolemize1 god) god (skolemize1 god))), % 6.84/3.31 inference(unit-propagation-resolution,[],[7,28,51,52]). % 6.84/3.31 cnf(54,axiom, % 6.84/3.31 ~((object X_6)) | ~((predicate7 X_5 X_5 X_6)) | ~((predicate6 X_5 X_5 X_6)) | (predicate8 X_6 X_5 X_6) | (predicate9 X_6 X_6 X_5), % 6.84/3.31 inference(axiom,[status(thm)],[]). % 6.84/3.31 cnf(55,plain, % 6.84/3.31 (predicate9 (skolemize1 god) (skolemize1 god) god), % 6.84/3.31 inference(unit-propagation-resolution,[],[7,28,35,53,54]). % 6.84/3.31 cnf(56,axiom, % 6.84/3.31 ~((predicate13 X_7 X_7)) | ~((predicate12 X_7 X_7)) | (exemplifies_relation greater_than (skolemize1 X_7) X_7), % 6.84/3.31 inference(axiom,[status(thm)],[]). % 6.84/3.31 cnf(57,plain, % 6.84/3.31 (exemplifies_relation greater_than (skolemize1 god) god), % 6.84/3.31 inference(unit-propagation-resolution,[],[30,33,56]). % 6.84/3.31 cnf(58,axiom, % 6.84/3.31 ~((exemplifies_relation greater_than X_6 X_5)) | ~((predicate9 X_6 X_6 X_5)) | ~((predicate7 X_5 X_5 X_6)) | ~((predicate6 X_5 X_5 X_6)) | (predicate8 X_6 X_5 X_6), % 6.84/3.31 inference(axiom,[status(thm)],[]). % 6.84/3.31 cnf(59,plain, % 6.84/3.31 ~((predicate9 (skolemize1 god) (skolemize1 god) god)), % 6.84/3.31 inference(unit-propagation-resolution,[],[7,28,57,53,58]). % 6.84/3.31 cnf(60,plain, % 6.84/3.31 $false, % 6.84/3.31 inference(conflict,[],[55,59]). % 6.84/3.31 cnf(61,plain, % 6.84/3.31 (predicate14 god god), % 6.84/3.31 inference(conflict-driven-clause-learning,[],[60]). % 6.84/3.32 cnf(62,plain, % 6.84/3.32 (predicate13 god god), % 6.84/3.32 inference(unit-propagation-resolution,[],[30,61,45,46]). % 6.84/3.32 cnf(63,plain, % 6.84/3.32 (object (skolemize1 god)), % 6.84/3.32 inference(unit-propagation-resolution,[],[30,62,34]). % 6.84/3.32 cnf(64,plain, % 6.84/3.32 (predicate9 (skolemize1 god) (skolemize1 god) god), % 6.84/3.32 inference(unit-propagation-resolution,[],[7,28,63,53,54]). % 6.84/3.32 cnf(65,plain, % 6.84/3.32 (exemplifies_relation greater_than (skolemize1 god) god), % 6.84/3.32 inference(unit-propagation-resolution,[],[30,62,56]). % 6.84/3.32 cnf(66,plain, % 6.84/3.32 ~((predicate9 (skolemize1 god) (skolemize1 god) god)), % 6.84/3.32 inference(unit-propagation-resolution,[],[7,28,65,53,58]). % 6.84/3.32 cnf(67,plain, % 6.84/3.32 $false, % 6.84/3.32 inference(conflict,[],[64,66]). % 6.84/3.32 % SZS output end CNFRefutation for Scavenger---EP-0.2_n077.star.cs.uiowa.edu_30326 % 6.84/3.34 % Scavenger ended %------------------------------------------------------------------------------