↑ Up

Fiesta---2.UNS-CRf.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : Fiesta---2
% Problem  : KLE090-10 : TPTP v8.1.0. Released v7.3.0.
% Transfm  : none
% Format   : dedam
% Command  : fiesta-wrapper %s

% Computer : n029.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  : 600s
% DateTime : Sun Jul 17 01:58:54 EDT 2022

% Result   : Unsatisfiable 18.64s 19.01s
% Output   : CNFRefutation 18.64s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12  % Problem  : KLE090-10 : TPTP v8.1.0. Released v7.3.0.
% 0.11/0.12  % Command  : fiesta-wrapper %s
% 0.12/0.34  % Computer : n029.cluster.edu
% 0.12/0.34  % Model    : x86_64 x86_64
% 0.12/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34  % Memory   : 8042.1875MB
% 0.12/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34  % CPULimit : 300
% 0.12/0.34  % WCLimit  : 600
% 0.12/0.34  % DateTime : Thu Jun 16 14:09:42 EDT 2022
% 0.12/0.34  % CPUTime  : 
% 18.64/19.01  Theorem Proved.
% 18.64/19.01  % SZS status Unsatisfiable
% 18.64/19.01  % SZS output start CNFRefutation
% 18.64/19.01  [1=axiom,[],
% 18.64/19.01  			addition(sK2_goals_X0,sK1_goals_X1) 	= sK1_goals_X1].
% 18.64/19.01  [2=axiom,[],
% 18.64/19.01  			coantidomain(coantidomain(X10)) 	= codomain(X10)].
% 18.64/19.01  [3=axiom,[2],
% 18.64/19.01  			addition(codomain(X10),coantidomain(X10)) 	= one].
% 18.64/19.01  [4=axiom,[2,2],
% 18.64/19.01  			addition(coantidomain(multiplication(X10,X11)),coantidomain(multiplication(codomain(X10),X11))) 	= coantidomain(multiplication(codomain(X10),X11))].
% 18.64/19.01  [5=axiom,[],
% 18.64/19.01  			multiplication(X10,coantidomain(X10)) 	= zero].
% 18.64/19.01  [6=axiom,[],
% 18.64/19.01  			antidomain(antidomain(X10)) 	= domain(X10)].
% 18.64/19.01  [7=axiom,[6],
% 18.64/19.01  			addition(domain(X10),antidomain(X10)) 	= one].
% 18.64/19.01  [8=axiom,[6,6],
% 18.64/19.01  			addition(antidomain(multiplication(X10,X11)),antidomain(multiplication(X10,domain(X11)))) 	= antidomain(multiplication(X10,domain(X11)))].
% 18.64/19.01  [9=axiom,[],
% 18.64/19.01  			multiplication(antidomain(X10),X10) 	= zero].
% 18.64/19.01  [12=axiom,[],
% 18.64/19.01  			multiplication(zero,X10) 	= zero].
% 18.64/19.01  [14=axiom,[],
% 18.64/19.01  			addition(multiplication(X10,X12),multiplication(X11,X12)) 	= multiplication(addition(X10,X11),X12)].
% 18.64/19.02  [15=axiom,[],
% 18.64/19.02  			addition(multiplication(X10,X11),multiplication(X10,X12)) 	= multiplication(X10,addition(X11,X12))].
% 18.64/19.02  [16=axiom,[],
% 18.64/19.02  			multiplication(one,X10) 	= X10].
% 18.64/19.02  [17=axiom,[],
% 18.64/19.02  			multiplication(X10,one) 	= X10].
% 18.64/19.02  [19=axiom,[],
% 18.64/19.02  			addition(X10,X10) 	= X10].
% 18.64/19.02  [20=axiom,[],
% 18.64/19.02  			addition(X10,zero) 	= X10].
% 18.64/19.02  [21=axiom,[],
% 18.64/19.02  			addition(addition(X10,X11),X12) 	= addition(X10,addition(X11,X12))].
% 18.64/19.02  [22=axiom,[],
% 18.64/19.02  			addition(X10,X11) 	= addition(X11,X10)].
% 18.64/19.02  [23=demod(1),[22],
% 18.64/19.02  			addition(sK1_goals_X1,sK2_goals_X0) 	= sK1_goals_X1].
% 18.64/19.02  [26=axiom,[],
% 18.64/19.02  			thtop(X10,X10) 	= thmfalse].
% 18.64/19.02  [27=axiom,[],
% 18.64/19.02  			thtop(addition(antidomain(sK1_goals_X1),antidomain(sK2_goals_X0)),antidomain(sK2_goals_X0)) 	= thmtrue].
% 18.64/19.02  [28=param(2,2),[],
% 18.64/19.02  			coantidomain(codomain(X10)) 	= codomain(coantidomain(X10))].
% 18.64/19.02  [33=param(6,6),[],
% 18.64/19.02  			antidomain(domain(X10)) 	= domain(antidomain(X10))].
% 18.64/19.02  [34=param(5,2),[],
% 18.64/19.02  			multiplication(coantidomain(X10),codomain(X10)) 	= zero].
% 18.64/19.02  [35=param(5,16),[],
% 18.64/19.02  			coantidomain(one) 	= zero].
% 18.64/19.02  [36=param(2,35),[],
% 18.64/19.02  			coantidomain(zero) 	= codomain(one)].
% 18.64/19.02  [38=param(3,35),[20],
% 18.64/19.02  			codomain(one) 	= one].
% 18.64/19.02  [40=demod(36),[38],
% 18.64/19.02  			coantidomain(zero) 	= one].
% 18.64/19.02  [49=param(4,9),[40],
% 18.64/19.02  			addition(one,coantidomain(multiplication(codomain(antidomain(X10)),X10))) 	= coantidomain(multiplication(codomain(antidomain(X10)),X10))].
% 18.64/19.02  [51=param(9,17),[],
% 18.64/19.02  			antidomain(one) 	= zero].
% 18.64/19.02  [58=param(6,51),[],
% 18.64/19.02  			antidomain(zero) 	= domain(one)].
% 18.64/19.02  [60=param(7,51),[20],
% 18.64/19.02  			domain(one) 	= one].
% 18.64/19.02  [62=demod(58),[60],
% 18.64/19.02  			antidomain(zero) 	= one].
% 18.64/19.02  [68=param(14,5),[],
% 18.64/19.02  			addition(zero,multiplication(X10,coantidomain(X11))) 	= multiplication(addition(X11,X10),coantidomain(X11))].
% 18.64/19.02  [71=param(14,9),[20],
% 18.64/19.02  			multiplication(addition(X10,antidomain(X11)),X11) 	= multiplication(X10,X11)].
% 18.64/19.02  [72=param(14,12),[],
% 18.64/19.02  			addition(zero,multiplication(X10,X11)) 	= multiplication(addition(zero,X10),X11)].
% 18.64/19.02  [73=demod(68),[72],
% 18.64/19.02  			multiplication(addition(zero,X10),coantidomain(X11)) 	= multiplication(addition(X11,X10),coantidomain(X11))].
% 18.64/19.02  [75=param(14,16),[],
% 18.64/19.02  			addition(X10,multiplication(X11,X10)) 	= multiplication(addition(one,X11),X10)].
% 18.64/19.02  [76=param(14,16),[22],
% 18.64/19.02  			addition(X10,multiplication(X11,X10)) 	= multiplication(addition(X11,one),X10)].
% 18.64/19.02  [80=param(15,5),[20],
% 18.64/19.02  			multiplication(X10,addition(X11,coantidomain(X10))) 	= multiplication(X10,X11)].
% 18.64/19.02  [81=param(15,9),[72],
% 18.64/19.02  			multiplication(addition(zero,antidomain(X10)),X11) 	= multiplication(antidomain(X10),addition(X10,X11))].
% 18.64/19.02  [84=param(15,17),[],
% 18.64/19.02  			addition(X10,multiplication(X10,X11)) 	= multiplication(X10,addition(one,X11))].
% 18.64/19.02  [85=param(15,17),[22],
% 18.64/19.02  			addition(X10,multiplication(X10,X11)) 	= multiplication(X10,addition(X11,one))].
% 18.64/19.02  [91=param(15,34),[20],
% 18.64/19.02  			multiplication(coantidomain(X10),addition(X11,codomain(X10))) 	= multiplication(coantidomain(X10),X11)].
% 18.64/19.02  [101=param(22,20),[],
% 18.64/19.02  			addition(zero,X10) 	= X10].
% 18.64/19.02  [103=demod(81),[101],
% 18.64/19.02  			multiplication(antidomain(X10),addition(X10,X11)) 	= multiplication(antidomain(X10),X11)].
% 18.64/19.02  [107=demod(73),[101],
% 18.64/19.02  			multiplication(addition(X11,X10),coantidomain(X11)) 	= multiplication(X10,coantidomain(X11))].
% 18.64/19.02  [111=param(21,7),[],
% 18.64/19.02  			addition(domain(X11),addition(antidomain(X11),X10)) 	= addition(one,X10)].
% 18.64/19.02  [115=param(21,19),[],
% 18.64/19.02  			addition(X10,addition(X10,X11)) 	= addition(X10,X11)].
% 18.64/19.02  [130=param(115,3),[22,3],
% 18.64/19.02  			addition(one,codomain(X10)) 	= one].
% 18.64/19.02  [134=param(115,22),[],
% 18.64/19.02  			addition(X10,addition(X11,X10)) 	= addition(X10,X11)].
% 18.64/19.02  [145=param(134,3),[22,22,3],
% 18.64/19.02  			addition(one,coantidomain(X10)) 	= one].
% 18.64/19.02  [146=demod(49),[145],
% 18.64/19.02  			coantidomain(multiplication(codomain(antidomain(X10)),X10)) 	= one].
% 18.64/19.02  [147=param(134,7),[22,22,7],
% 18.64/19.02  			addition(one,antidomain(X10)) 	= one].
% 18.64/19.02  [165=param(5,146),[17],
% 18.64/19.02  			multiplication(codomain(antidomain(X10)),X10) 	= zero].
% 18.64/19.02  [176=param(14,165),[101],
% 18.64/19.02  			multiplication(addition(codomain(antidomain(X11)),X10),X11) 	= multiplication(X10,X11)].
% 18.64/19.02  [307=param(71,7),[16],
% 18.64/19.02  			multiplication(domain(X10),X10) 	= X10].
% 18.64/19.02  [382=param(80,3),[17],
% 18.64/19.02  			multiplication(X10,codomain(X10)) 	= X10].
% 18.64/19.02  [395=param(76,382),[22],
% 18.64/19.02  			addition(X10,codomain(X10)) 	= multiplication(addition(X10,one),codomain(X10))].
% 18.64/19.02  [439=param(84,147),[17],
% 18.64/19.02  			addition(X10,multiplication(X10,antidomain(X11))) 	= X10].
% 18.64/19.02  [458=param(85,307),[22],
% 18.64/19.02  			addition(X10,domain(X10)) 	= multiplication(domain(X10),addition(X10,one))].
% 18.64/19.02  [654=param(103,7),[33,17,33,307],
% 18.64/19.02  			domain(antidomain(X10)) 	= antidomain(X10)].
% 18.64/19.02  [655=demod(33),[654],
% 18.64/19.02  			antidomain(domain(X10)) 	= antidomain(X10)].
% 18.64/19.02  [658=param(103,23),[9],
% 18.64/19.02  			multiplication(antidomain(sK1_goals_X1),sK2_goals_X0) 	= zero].
% 18.64/19.02  [677=param(8,658),[62,147],
% 18.64/19.02  			antidomain(multiplication(antidomain(sK1_goals_X1),domain(sK2_goals_X0))) 	= one].
% 18.64/19.02  [697=param(9,677),[16],
% 18.64/19.02  			multiplication(antidomain(sK1_goals_X1),domain(sK2_goals_X0)) 	= zero].
% 18.64/19.02  [709=param(15,697),[101],
% 18.64/19.02  			multiplication(antidomain(sK1_goals_X1),addition(domain(sK2_goals_X0),X10)) 	= multiplication(antidomain(sK1_goals_X1),X10)].
% 18.64/19.02  [717=param(107,3),[28,16,28,382],
% 18.64/19.02  			codomain(coantidomain(X10)) 	= coantidomain(X10)].
% 18.64/19.02  [1014=param(111,395),[22,147,16,130],
% 18.64/19.02  			addition(domain(X10),codomain(antidomain(X10))) 	= one].
% 18.64/19.02  [1026=param(91,1014),[17],
% 18.64/19.02  			multiplication(coantidomain(antidomain(X10)),domain(X10)) 	= coantidomain(antidomain(X10))].
% 18.64/19.02  [1043=param(176,3),[16],
% 18.64/19.02  			multiplication(coantidomain(antidomain(X10)),X10) 	= X10].
% 18.64/19.02  [1054=param(8,1043),[655,1043,655,19,655,1026],
% 18.64/19.02  			antidomain(coantidomain(antidomain(X10))) 	= antidomain(X10)].
% 18.64/19.02  [1062=param(439,1043),[6,6],
% 18.64/19.02  			addition(coantidomain(domain(X10)),antidomain(X10)) 	= coantidomain(domain(X10))].
% 18.64/19.02  [1064=param(6,1054),[6],
% 18.64/19.02  			domain(coantidomain(antidomain(X10))) 	= domain(X10)].
% 18.64/19.02  [1066=param(1064,6),[654],
% 18.64/19.02  			antidomain(X10) 	= domain(coantidomain(domain(X10)))].
% 18.64/19.02  [1068=demod(1062),[1066,458,22,145,17],
% 18.64/19.02  			domain(coantidomain(domain(X10))) 	= coantidomain(domain(X10))].
% 18.64/19.02  [1069=demod(1066),[1068],
% 18.64/19.02  			antidomain(X10) 	= coantidomain(domain(X10))].
% 18.64/19.02  [1083=demod(1014),[1069,717],
% 18.64/19.02  			addition(domain(X10),coantidomain(domain(X10))) 	= one].
% 18.64/19.02  [1206=demod(709),[1069,1069],
% 18.64/19.02  			multiplication(coantidomain(domain(sK1_goals_X1)),addition(domain(sK2_goals_X0),X10)) 	= multiplication(coantidomain(domain(sK1_goals_X1)),X10)].
% 18.64/19.02  [1216=param(27,1069),[1069,1069],
% 18.64/19.02  			thtop(addition(coantidomain(domain(sK1_goals_X1)),coantidomain(domain(sK2_goals_X0))),coantidomain(domain(sK2_goals_X0))) 	= thmtrue].
% 18.64/19.02  [29250=param(1206,1083),[17],
% 18.64/19.02  			multiplication(coantidomain(domain(sK1_goals_X1)),coantidomain(domain(sK2_goals_X0))) 	= coantidomain(domain(sK1_goals_X1))].
% 18.64/19.02  [29260=param(75,29250),[22,145,16],
% 18.64/19.02  			addition(coantidomain(domain(sK1_goals_X1)),coantidomain(domain(sK2_goals_X0))) 	= coantidomain(domain(sK2_goals_X0))].
% 18.64/19.02  [29616=param(1216,29260),[26],
% 18.64/19.02  			thmtrue 	= thmfalse].
% 18.64/19.02  % SZS output end CNFRefutation
% 18.64/19.02  Space: 118252 KB 
%------------------------------------------------------------------------------