↑ Up

Fiesta---2.UNS-CRf.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : Fiesta---2
% Problem  : LAT021-1 : TPTP v8.1.0. Released v2.2.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:55:26 EDT 2022

% Result   : Unsatisfiable 1.19s 1.58s
% Output   : CNFRefutation 1.19s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12  % Problem  : LAT021-1 : TPTP v8.1.0. Released v2.2.0.
% 0.04/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 : Thu Jun 30 03:12:23 EDT 2022
% 0.12/0.33  % CPUTime  : 
% 1.19/1.58  Theorem Proved.
% 1.19/1.58  % SZS status Unsatisfiable
% 1.19/1.58  % SZS output start CNFRefutation
% 1.19/1.58  [1=axiom,[],
% 1.19/1.58  			join(join(X10,meet(X11,X12)),meet(join(X10,X11),X12)) 	= join(X10,meet(X11,X12))].
% 1.19/1.58  [2=axiom,[],
% 1.19/1.58  			meet(join(X10,meet(X11,X12)),join(X10,X11)) 	= join(X10,meet(X11,X12))].
% 1.19/1.58  [3=axiom,[],
% 1.19/1.58  			join(meet(X10,join(X11,X12)),meet(X10,X11)) 	= meet(X10,join(X11,X12))].
% 1.19/1.58  [4=axiom,[],
% 1.19/1.58  			join(join(X10,X11),X12) 	= join(X10,join(X11,X12))].
% 1.19/1.58  [5=demod(1),[4],
% 1.19/1.58  			join(X10,join(meet(X11,X12),meet(join(X10,X11),X12))) 	= join(X10,meet(X11,X12))].
% 1.19/1.58  [6=axiom,[],
% 1.19/1.58  			meet(meet(X10,X11),X12) 	= meet(X10,meet(X11,X12))].
% 1.19/1.58  [7=axiom,[],
% 1.19/1.58  			join(X10,X11) 	= join(X11,X10)].
% 1.19/1.58  [8=demod(3),[7],
% 1.19/1.58  			join(meet(X10,X11),meet(X10,join(X11,X12))) 	= meet(X10,join(X11,X12))].
% 1.19/1.58  [9=axiom,[],
% 1.19/1.58  			meet(X10,X11) 	= meet(X11,X10)].
% 1.19/1.58  [10=demod(2),[9],
% 1.19/1.58  			meet(join(X10,X11),join(X10,meet(X11,X12))) 	= join(X10,meet(X11,X12))].
% 1.19/1.58  [11=axiom,[],
% 1.19/1.58  			join(X10,X10) 	= X10].
% 1.19/1.58  [12=axiom,[],
% 1.19/1.58  			meet(X10,X10) 	= X10].
% 1.19/1.58  [13=axiom,[],
% 1.19/1.58  			thtop(X10,X10) 	= thmfalse].
% 1.19/1.58  [14=axiom,[7,9,9,7],
% 1.19/1.58  			thtop(meet(a,join(c,b)),join(meet(c,a),meet(b,a))) 	= thmtrue].
% 1.19/1.58  [16=param(4,11),[],
% 1.19/1.58  			join(X10,join(X10,X11)) 	= join(X10,X11)].
% 1.19/1.58  [17=param(7,4),[],
% 1.19/1.58  			join(X10,join(X11,X12)) 	= join(X11,join(X12,X10))].
% 1.19/1.58  [18=param(4,7),[4],
% 1.19/1.58  			join(X10,join(X11,X12)) 	= join(X11,join(X10,X12))].
% 1.19/1.58  [20=param(16,7),[4],
% 1.19/1.58  			join(X10,join(X11,X10)) 	= join(X10,X11)].
% 1.19/1.58  [21=param(5,12),[9,12],
% 1.19/1.58  			join(X10,join(X11,meet(X11,join(X10,X11)))) 	= join(X10,X11)].
% 1.19/1.58  [22=param(5,12),[17,21,16],
% 1.19/1.58  			join(X10,meet(X11,join(X10,X11))) 	= join(X10,X11)].
% 1.19/1.58  [23=param(5,16),[11,7,9],
% 1.19/1.58  			join(meet(X10,X11),meet(X11,join(X10,meet(X10,X11)))) 	= meet(X10,X11)].
% 1.19/1.58  [25=param(20,4),[],
% 1.19/1.58  			join(X10,join(X11,join(X12,X10))) 	= join(X10,join(X11,X12))].
% 1.19/1.58  [28=param(6,9),[6],
% 1.19/1.58  			meet(X10,meet(X11,X12)) 	= meet(X11,meet(X10,X12))].
% 1.19/1.58  [30=param(6,12),[],
% 1.19/1.58  			meet(X10,meet(X10,X11)) 	= meet(X10,X11)].
% 1.19/1.58  [31=param(8,7),[],
% 1.19/1.58  			join(meet(X10,X11),meet(X10,join(X12,X11))) 	= meet(X10,join(X11,X12))].
% 1.19/1.58  [32=param(8,9),[],
% 1.19/1.58  			join(meet(X10,X11),meet(X11,join(X10,X12))) 	= meet(X11,join(X10,X12))].
% 1.19/1.58  [33=demod(23),[32],
% 1.19/1.58  			meet(X10,join(X11,meet(X11,X10))) 	= meet(X11,X10)].
% 1.19/1.58  [34=param(8,9),[],
% 1.19/1.58  			join(meet(X10,X11),meet(join(X11,X12),X10)) 	= meet(X10,join(X11,X12))].
% 1.19/1.58  [36=param(8,12),[9,17,12],
% 1.19/1.58  			join(X10,join(X11,meet(X10,join(X10,X11)))) 	= join(X10,X11)].
% 1.19/1.58  [38=param(30,9),[6],
% 1.19/1.58  			meet(X10,meet(X11,X10)) 	= meet(X10,X11)].
% 1.19/1.58  [40=param(38,6),[],
% 1.19/1.58  			meet(X10,meet(X11,meet(X12,X10))) 	= meet(X10,meet(X11,X12))].
% 1.19/1.58  [44=param(10,9),[],
% 1.19/1.58  			meet(join(X10,X11),join(X10,meet(X12,X11))) 	= join(X10,meet(X11,X12))].
% 1.19/1.58  [47=param(8,33),[33],
% 1.19/1.58  			join(meet(X10,X11),meet(X11,X10)) 	= meet(X11,X10)].
% 1.19/1.58  [62=param(18,22),[],
% 1.19/1.58  			join(X11,join(X10,meet(X12,join(X11,X12)))) 	= join(X10,join(X11,X12))].
% 1.19/1.58  [63=param(18,47),[],
% 1.19/1.58  			join(meet(X12,X11),join(X10,meet(X11,X12))) 	= join(X10,meet(X11,X12))].
% 1.19/1.58  [67=param(25,47),[20,63],
% 1.19/1.58  			join(meet(X10,X11),X12) 	= join(X12,meet(X11,X10))].
% 1.19/1.58  [112=param(31,12),[9,17,62,20],
% 1.19/1.58  			meet(join(X11,X10),join(X10,X11)) 	= join(X10,X11)].
% 1.19/1.58  [115=param(31,7),[],
% 1.19/1.58  			join(meet(X10,X12),meet(X10,join(X11,X12))) 	= meet(X10,join(X11,X12))].
% 1.19/1.58  [117=param(5,112),[17,36,20],
% 1.19/1.58  			join(X10,meet(X11,join(X11,X10))) 	= join(X10,X11)].
% 1.19/1.58  [120=param(28,112),[],
% 1.19/1.58  			meet(join(X12,X11),meet(X10,join(X11,X12))) 	= meet(X10,join(X11,X12))].
% 1.19/1.58  [121=param(40,112),[38,120],
% 1.19/1.58  			meet(join(X10,X11),X12) 	= meet(X12,join(X11,X10))].
% 1.19/1.58  [124=param(18,117),[],
% 1.19/1.58  			join(X11,join(X10,meet(X12,join(X12,X11)))) 	= join(X10,join(X11,X12))].
% 1.19/1.58  [127=param(5,121),[32],
% 1.19/1.58  			join(X10,meet(X11,join(X12,X10))) 	= join(X10,meet(X12,X11))].
% 1.19/1.58  [155=param(34,9),[],
% 1.19/1.58  			join(meet(X10,X11),meet(join(X11,X12),X10)) 	= meet(join(X11,X12),X10)].
% 1.19/1.58  [188=param(155,7),[-67],
% 1.19/1.58  			join(meet(X10,X12),meet(join(X10,X11),X12)) 	= meet(join(X10,X11),X12)].
% 1.19/1.58  [204=param(124,115),[127,12,17],
% 1.19/1.58  			join(X10,join(X11,meet(X11,X10))) 	= join(X10,X11)].
% 1.19/1.58  [206=param(204,7),[4,7],
% 1.19/1.58  			join(X11,join(X10,meet(X11,X10))) 	= join(X10,X11)].
% 1.19/1.58  [225=param(155,206),[206],
% 1.19/1.58  			join(meet(X10,X11),meet(join(X12,X11),X10)) 	= meet(join(X12,X11),X10)].
% 1.19/1.58  [226=param(188,206),[206],
% 1.19/1.58  			join(meet(X10,X11),meet(join(X12,X10),X11)) 	= meet(join(X12,X10),X11)].
% 1.19/1.58  [227=demod(5),[226],
% 1.19/1.58  			join(X10,meet(join(X10,X11),X12)) 	= join(X10,meet(X11,X12))].
% 1.19/1.58  [235=param(44,227),[44],
% 1.19/1.58  			join(X10,meet(X11,join(X10,X12))) 	= join(X10,meet(X11,X12))].
% 1.19/1.58  [370=param(225,30),[121,235,121],
% 1.19/1.58  			meet(X10,join(meet(X10,X11),X12)) 	= join(meet(X10,X11),meet(X10,X12))].
% 1.19/1.58  [374=param(370,67),[],
% 1.19/1.58  			meet(X10,join(X11,meet(X12,X10))) 	= join(meet(X10,X12),meet(X10,X11))].
% 1.19/1.58  [375=param(374,227),[374,7,8],
% 1.19/1.58  			meet(X10,join(X12,X11)) 	= join(meet(X10,X11),meet(X10,X12))].
% 1.19/1.58  [417=param(14,375),[9,9,7,13],
% 1.19/1.58  			thmtrue 	= thmfalse].
% 1.19/1.58  % SZS output end CNFRefutation
% 1.19/1.58  Space:   1626 KB 
%------------------------------------------------------------------------------