↑ Up

Fiesta---2.UNS-CRf.s

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

% Computer : n008.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 04:58:32 EDT 2022

% Result   : Unsatisfiable 128.23s 128.65s
% Output   : CNFRefutation 128.23s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12  % Problem  : LAT399-2 : TPTP v8.1.0. Released v8.1.0.
% 0.11/0.12  % Command  : fiesta-wrapper %s
% 0.12/0.33  % Computer : n008.cluster.edu
% 0.12/0.33  % Model    : x86_64 x86_64
% 0.12/0.33  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33  % Memory   : 8042.1875MB
% 0.12/0.33  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33  % CPULimit : 300
% 0.12/0.33  % WCLimit  : 600
% 0.12/0.33  % DateTime : Wed Jun 29 13:45:38 EDT 2022
% 0.12/0.33  % CPUTime  : 
% 128.23/128.65  Theorem Proved.
% 128.23/128.65  % SZS status Unsatisfiable
% 128.23/128.65  % SZS output start CNFRefutation
% 128.23/128.65  [1=axiom,[],
% 128.23/128.65  			join(upme(meet(a,X10),X11,X12),meet(X11,X12)) 	= meet(join(meet(meet(a,X10),X11),X12),join(meet(meet(a,X10),X12),X11))].
% 128.23/128.65  [4=axiom,[],
% 128.23/128.65  			lome(X10,X11,X12) 	= join(meet(X10,X11),meet(X10,X12))].
% 128.23/128.65  [5=axiom,[],
% 128.23/128.65  			upme(X10,X11,X12) 	= meet(X10,join(X11,X12))].
% 128.23/128.65  [6=demod(1),[5],
% 128.23/128.65  			meet(join(meet(meet(a,X10),X11),X12),join(meet(meet(a,X10),X12),X11)) 	= join(meet(meet(a,X10),join(X11,X12)),meet(X11,X12))].
% 128.23/128.65  [7=axiom,[],
% 128.23/128.65  			meet(X10,join(X10,X11)) 	= X10].
% 128.23/128.65  [8=axiom,[],
% 128.23/128.65  			join(X10,meet(X10,X11)) 	= X10].
% 128.23/128.65  [9=axiom,[],
% 128.23/128.65  			join(join(X10,X11),X12) 	= join(X10,join(X11,X12))].
% 128.23/128.65  [10=axiom,[],
% 128.23/128.65  			join(X10,X11) 	= join(X11,X10)].
% 128.23/128.65  [11=axiom,[],
% 128.23/128.65  			meet(meet(X10,X11),X12) 	= meet(X10,meet(X11,X12))].
% 128.23/128.65  [12=demod(6),[11,11,11],
% 128.23/128.65  			meet(join(meet(a,meet(X10,X11)),X12),join(meet(a,meet(X10,X12)),X11)) 	= join(meet(a,meet(X10,join(X11,X12))),meet(X11,X12))].
% 128.23/128.65  [13=axiom,[],
% 128.23/128.65  			meet(X10,X11) 	= meet(X11,X10)].
% 128.23/128.65  [14=axiom,[],
% 128.23/128.65  			thtop(X10,X10) 	= thmfalse].
% 128.23/128.65  [15=axiom,[13,5,10,11,13,4,11,13,11,13,10],
% 128.23/128.65  			thtop(meet(z1,meet(a,join(z3,z2))),join(meet(z1,meet(z3,a)),meet(z1,meet(z2,a)))) 	= thmtrue].
% 128.23/128.65  [18=param(8,13),[],
% 128.23/128.65  			join(X10,meet(X11,X10)) 	= X10].
% 128.23/128.65  [19=param(15,13),[11,13],
% 128.23/128.65  			thtop(meet(a,meet(z1,join(z3,z2))),join(meet(z1,meet(z3,a)),meet(z1,meet(z2,a)))) 	= thmtrue].
% 128.23/128.65  [25=param(7,10),[],
% 128.23/128.65  			meet(X10,join(X11,X10)) 	= X10].
% 128.23/128.65  [27=param(25,8),[11],
% 128.23/128.65  			meet(X10,meet(X11,X10)) 	= meet(X10,X11)].
% 128.23/128.65  [28=param(18,25),[10],
% 128.23/128.65  			join(X10,join(X11,X10)) 	= join(X11,X10)].
% 128.23/128.65  [30=param(27,13),[],
% 128.23/128.65  			meet(X10,meet(X10,X11)) 	= meet(X10,X11)].
% 128.23/128.65  [31=param(18,27),[],
% 128.23/128.65  			join(meet(X10,X11),meet(X11,X10)) 	= meet(X10,X11)].
% 128.23/128.65  [35=param(11,13),[],
% 128.23/128.65  			meet(X10,meet(X11,X12)) 	= meet(X12,meet(X10,X11))].
% 128.23/128.65  [37=param(18,11),[],
% 128.23/128.65  			join(X10,meet(X11,meet(X12,X10))) 	= X10].
% 128.23/128.65  [41=param(11,27),[11,11],
% 128.23/128.65  			meet(X10,meet(X11,meet(X10,X12))) 	= meet(X10,meet(X11,X12))].
% 128.23/128.65  [43=param(37,7),[9],
% 128.23/128.65  			join(X10,join(X11,meet(X12,X10))) 	= join(X10,X11)].
% 128.23/128.65  [45=param(37,13),[11],
% 128.23/128.65  			join(X10,meet(X11,meet(X10,X12))) 	= X10].
% 128.23/128.65  [47=param(45,11),[],
% 128.23/128.65  			join(X10,meet(X11,meet(X12,meet(X10,X13)))) 	= X10].
% 128.23/128.65  [48=param(45,11),[],
% 128.23/128.65  			join(meet(X10,X11),meet(X12,meet(X10,meet(X11,X13)))) 	= meet(X10,X11)].
% 128.23/128.65  [49=param(7,9),[],
% 128.23/128.65  			meet(join(X10,X11),join(X10,join(X11,X12))) 	= join(X10,X11)].
% 128.23/128.65  [50=param(9,8),[],
% 128.23/128.65  			join(X10,join(X11,meet(join(X10,X11),X12))) 	= join(X10,X11)].
% 128.23/128.65  [51=param(9,8),[],
% 128.23/128.65  			join(X10,join(meet(X10,X12),X11)) 	= join(X10,X11)].
% 128.23/128.65  [52=param(9,10),[],
% 128.23/128.65  			join(X10,join(X11,X12)) 	= join(X12,join(X10,X11))].
% 128.23/128.65  [53=param(9,10),[9],
% 128.23/128.65  			join(X10,join(X11,X12)) 	= join(X11,join(X10,X12))].
% 128.23/128.65  [55=param(9,18),[],
% 128.23/128.65  			join(X10,join(meet(X12,X10),X11)) 	= join(X10,X11)].
% 128.23/128.65  [57=param(25,9),[],
% 128.23/128.65  			meet(X10,join(X11,join(X12,X10))) 	= X10].
% 128.23/128.65  [64=param(57,8),[11],
% 128.23/128.65  			meet(X10,meet(X11,join(X12,X10))) 	= meet(X10,X11)].
% 128.23/128.65  [69=param(18,57),[10],
% 128.23/128.65  			join(X10,join(X11,join(X12,X10))) 	= join(X11,join(X12,X10))].
% 128.23/128.65  [75=param(64,10),[],
% 128.23/128.65  			meet(X10,meet(X11,join(X10,X12))) 	= meet(X10,X11)].
% 128.23/128.65  [81=param(18,75),[],
% 128.23/128.65  			join(meet(X10,join(X11,X12)),meet(X11,X10)) 	= meet(X10,join(X11,X12))].
% 128.23/128.65  [88=param(25,55),[13],
% 128.23/128.65  			meet(join(X10,X11),join(meet(X12,X10),X11)) 	= join(meet(X12,X10),X11)].
% 128.23/128.65  [90=param(25,51),[13],
% 128.23/128.65  			meet(join(X10,X11),join(meet(X10,X12),X11)) 	= join(meet(X10,X12),X11)].
% 128.23/128.65  [92=param(43,9),[],
% 128.23/128.65  			join(X10,join(X11,join(X12,meet(X13,X10)))) 	= join(X10,join(X11,X12))].
% 128.23/128.65  [95=param(25,43),[],
% 128.23/128.65  			meet(join(X10,meet(X11,X12)),join(X12,X10)) 	= join(X10,meet(X11,X12))].
% 128.23/128.65  [96=param(43,27),[],
% 128.23/128.65  			join(meet(X10,X11),join(X12,meet(X11,X10))) 	= join(meet(X10,X11),X12)].
% 128.23/128.65  [105=param(69,31),[96,31],
% 128.23/128.65  			join(meet(X10,X11),X12) 	= join(X12,meet(X11,X10))].
% 128.23/128.65  [107=demod(81),[-105],
% 128.23/128.65  			join(meet(X10,X11),meet(X10,join(X11,X12))) 	= meet(X10,join(X11,X12))].
% 128.23/128.65  [112=param(35,11),[11],
% 128.23/128.65  			meet(X10,meet(X11,meet(X12,X13))) 	= meet(X11,meet(X12,meet(X13,X10)))].
% 128.23/128.65  [121=param(35,64),[],
% 128.23/128.65  			meet(join(X10,X11),meet(X11,X12)) 	= meet(X11,X12)].
% 128.23/128.65  [162=param(105,41),[11,11,27],
% 128.23/128.65  			join(meet(X10,meet(X11,X12)),X13) 	= join(X13,meet(X11,meet(X10,X12)))].
% 128.23/128.65  [168=param(105,10),[],
% 128.23/128.67  			join(meet(X10,X11),X12) 	= join(meet(X11,X10),X12)].
% 128.23/128.67  [185=param(49,10),[],
% 128.23/128.67  			meet(join(X10,X11),join(X10,join(X12,X11))) 	= join(X10,X11)].
% 128.23/128.67  [186=param(49,28),[],
% 128.23/128.67  			meet(join(X10,X11),join(X11,X10)) 	= join(X10,X11)].
% 128.23/128.67  [190=param(11,186),[],
% 128.23/128.67  			meet(join(X10,X11),meet(join(X11,X10),X12)) 	= meet(join(X10,X11),X12)].
% 128.23/128.67  [191=param(35,186),[],
% 128.23/128.67  			meet(join(X12,X11),meet(X10,join(X11,X12))) 	= meet(X10,join(X11,X12))].
% 128.23/128.67  [194=param(41,186),[27,191],
% 128.23/128.67  			meet(join(X10,X11),X12) 	= meet(X12,join(X11,X10))].
% 128.23/128.67  [196=demod(95),[-194],
% 128.23/128.67  			meet(join(X10,X11),join(X10,meet(X12,X11))) 	= join(X10,meet(X12,X11))].
% 128.23/128.67  [217=param(57,50),[-194,190],
% 128.23/128.67  			meet(join(X10,X11),X12) 	= meet(join(X11,X10),X12)].
% 128.23/128.67  [219=param(217,9),[],
% 128.23/128.67  			meet(join(X10,join(X11,X12)),X13) 	= meet(join(X12,join(X10,X11)),X13)].
% 128.23/128.67  [277=param(53,47),[],
% 128.23/128.67  			join(X11,join(X10,meet(X12,meet(X13,meet(X11,X14))))) 	= join(X10,X11)].
% 128.23/128.67  [292=param(185,8),[194],
% 128.23/128.67  			meet(join(X10,X11),join(meet(X11,X12),X10)) 	= join(X10,meet(X11,X12))].
% 128.23/128.67  [314=param(45,292),[9],
% 128.23/128.67  			join(X10,join(X11,meet(X12,join(X10,meet(X11,X13))))) 	= join(X10,X11)].
% 128.23/128.67  [368=param(314,194),[],
% 128.23/128.67  			join(X10,join(X11,meet(join(meet(X11,X12),X10),X13))) 	= join(X10,X11)].
% 128.23/128.67  [381=param(368,168),[],
% 128.23/128.67  			join(X10,join(X11,meet(join(meet(X12,X11),X10),X13))) 	= join(X10,X11)].
% 128.23/128.67  [410=param(12,27),[10,8,194,75],
% 128.23/128.67  			meet(a,join(X10,meet(a,X11))) 	= join(meet(a,X11),meet(a,X10))].
% 128.23/128.67  [765=param(90,8),[],
% 128.23/128.67  			meet(X10,join(meet(X10,X11),meet(X10,X12))) 	= join(meet(X10,X11),meet(X10,X12))].
% 128.23/128.67  [1334=param(219,121),[],
% 128.23/128.67  			meet(join(X10,join(X11,X12)),meet(join(X10,X11),X13)) 	= meet(join(X10,X11),X13)].
% 128.23/128.67  [1342=param(1334,196),[196],
% 128.23/128.67  			meet(join(X10,join(X11,X12)),join(X10,meet(X13,X11))) 	= join(X10,meet(X13,X11))].
% 128.23/128.67  [1371=param(1342,52),[],
% 128.23/128.67  			meet(join(X10,join(X11,X12)),join(X11,meet(X13,X12))) 	= join(X11,meet(X13,X12))].
% 128.23/128.67  [1704=param(53,48),[],
% 128.23/128.67  			join(meet(X11,X12),join(X10,meet(X13,meet(X11,meet(X12,X14))))) 	= join(X10,meet(X11,X12))].
% 128.23/128.67  [3363=param(381,12),[92],
% 128.23/128.67  			join(X10,join(meet(X11,X12),meet(a,meet(X11,join(X12,X10))))) 	= join(X10,meet(X11,X12))].
% 128.23/128.67  [4503=param(1371,55),[],
% 128.23/128.67  			meet(join(X10,X11),join(meet(X12,X10),meet(X13,X11))) 	= join(meet(X12,X10),meet(X13,X11))].
% 128.23/128.67  [6434=param(3363,30),[107],
% 128.23/128.67  			join(X10,meet(a,join(X11,X10))) 	= join(X10,meet(a,X11))].
% 128.23/128.67  [6438=param(57,3363),[-194,112,88],
% 128.23/128.67  			meet(a,meet(X10,join(meet(X10,X11),X12))) 	= meet(a,meet(X10,join(X11,X12)))].
% 128.23/128.67  [6452=param(25,6434),[-194,35,194,410,4503],
% 128.23/128.67  			meet(a,join(X10,X11)) 	= join(meet(a,X10),meet(a,X11))].
% 128.23/128.67  [6562=param(6438,1704),[277],
% 128.23/128.67  			meet(a,meet(X10,join(X11,meet(X10,X12)))) 	= meet(a,meet(X10,join(X11,X12)))].
% 128.23/128.67  [6576=param(6562,765),[6452,6438],
% 128.23/128.67  			meet(a,meet(X10,join(X11,X12))) 	= join(meet(a,meet(X10,X11)),meet(a,meet(X10,X12)))].
% 128.23/128.67  [6585=param(19,6576),[13,35,13,13,35,13,-162,-162,-162,-162,14],
% 128.23/128.67  			thmtrue 	= thmfalse].
% 128.23/128.67  % SZS output end CNFRefutation
% 128.23/128.67  Space: 231471 KB 
%------------------------------------------------------------------------------