↑ Up

Fiesta---2.UNS-CRf.s

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

% Computer : n012.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 : Sat Jul 16 09:15:31 EDT 2022

% Result   : Unsatisfiable 2.75s 3.17s
% Output   : CNFRefutation 2.75s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12  % Problem  : GRP707-1 : TPTP v8.1.0. Released v4.0.0.
% 0.11/0.12  % Command  : fiesta-wrapper %s
% 0.12/0.33  % Computer : n012.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 : Tue Jun 14 07:46:10 EDT 2022
% 0.12/0.34  % CPUTime  : 
% 2.75/3.17  Theorem Proved.
% 2.75/3.17  % SZS status Unsatisfiable
% 2.75/3.17  % SZS output start CNFRefutation
% 2.75/3.17  [1=axiom,[],
% 2.75/3.17  			mult(mult(X10,X10),X11) 	= mult(X11,mult(X10,X10))].
% 2.75/3.17  [2=axiom,[],
% 2.75/3.17  			mult(X10,mult(X10,mult(X10,X10))) 	= unit].
% 2.75/3.17  [3=axiom,[],
% 2.75/3.17  			mult(mult(mult(X10,X11),X11),X12) 	= mult(X10,mult(X11,mult(X11,X12)))].
% 2.75/3.17  [4=axiom,[],
% 2.75/3.17  			mult(unit,X10) 	= X10].
% 2.75/3.17  [5=axiom,[],
% 2.75/3.17  			mult(X10,unit) 	= X10].
% 2.75/3.17  [6=axiom,[],
% 2.75/3.17  			rd(mult(X10,X11),X11) 	= X10].
% 2.75/3.17  [7=axiom,[],
% 2.75/3.17  			mult(rd(X10,X11),X11) 	= X10].
% 2.75/3.17  [8=axiom,[],
% 2.75/3.17  			ld(X10,mult(X10,X11)) 	= X11].
% 2.75/3.17  [9=axiom,[],
% 2.75/3.17  			mult(X10,ld(X10,X11)) 	= X11].
% 2.75/3.17  [10=axiom,[],
% 2.75/3.17  			thtop(X10,X10) 	= thmfalse].
% 2.75/3.17  [11=axiom,[],
% 2.75/3.17  			thtop(mult(mult(a,b),a),mult(a,mult(b,a))) 	= thmtrue].
% 2.75/3.17  [13=param(8,1),[],
% 2.75/3.17  			ld(mult(X10,X10),mult(X11,mult(X10,X10))) 	= X11].
% 2.75/3.17  [16=param(8,2),[],
% 2.75/3.17  			ld(X10,unit) 	= mult(X10,mult(X10,X10))].
% 2.75/3.17  [18=param(3,4),[4],
% 2.75/3.17  			mult(mult(X10,X10),X11) 	= mult(X10,mult(X10,X11))].
% 2.75/3.17  [19=demod(1),[18],
% 2.75/3.17  			mult(X10,mult(X10,X11)) 	= mult(X11,mult(X10,X10))].
% 2.75/3.17  [21=param(3,5),[5],
% 2.75/3.17  			mult(mult(X10,X11),X11) 	= mult(X10,mult(X11,X11))].
% 2.75/3.17  [22=demod(3),[21],
% 2.75/3.17  			mult(mult(X10,mult(X11,X11)),X12) 	= mult(X10,mult(X11,mult(X11,X12)))].
% 2.75/3.17  [23=param(7,5),[],
% 2.75/3.17  			rd(X10,unit) 	= X10].
% 2.75/3.17  [24=param(8,7),[],
% 2.75/3.17  			ld(rd(X10,X11),X10) 	= X11].
% 2.75/3.17  [25=param(6,2),[],
% 2.75/3.17  			rd(unit,mult(X10,mult(X10,X10))) 	= X10].
% 2.75/3.17  [26=param(6,4),[],
% 2.75/3.17  			rd(X10,X10) 	= unit].
% 2.75/3.17  [27=param(6,9),[],
% 2.75/3.17  			rd(X10,ld(X11,X10)) 	= X11].
% 2.75/3.17  [28=param(13,7),[],
% 2.75/3.17  			ld(mult(X10,X10),X11) 	= rd(X11,mult(X10,X10))].
% 2.75/3.17  [30=param(28,8),[18],
% 2.75/3.17  			rd(mult(X10,mult(X10,X11)),mult(X10,X10)) 	= X11].
% 2.75/3.17  [32=param(28,16),[18,2,18,5],
% 2.75/3.17  			rd(unit,mult(X10,X10)) 	= mult(X10,X10)].
% 2.75/3.17  [33=param(6,18),[],
% 2.75/3.17  			rd(mult(X10,mult(X10,X11)),X11) 	= mult(X10,X10)].
% 2.75/3.17  [35=param(6,19),[],
% 2.75/3.17  			rd(mult(X10,mult(X11,X11)),mult(X11,X10)) 	= X11].
% 2.75/3.17  [37=param(8,19),[],
% 2.75/3.17  			ld(X10,mult(X11,mult(X10,X10))) 	= mult(X10,X11)].
% 2.75/3.17  [38=param(19,19),[],
% 2.75/3.17  			mult(mult(X10,X11),mult(X10,X10)) 	= mult(X10,mult(X11,mult(X10,X10)))].
% 2.75/3.17  [41=param(6,21),[],
% 2.75/3.17  			rd(mult(X10,mult(X11,X11)),X11) 	= mult(X10,X11)].
% 2.75/3.17  [42=param(21,7),[],
% 2.75/3.17  			mult(rd(X10,X11),mult(X11,X11)) 	= mult(X10,X11)].
% 2.75/3.17  [47=param(21,21),[22],
% 2.75/3.17  			mult(mult(X10,X11),mult(X11,X11)) 	= mult(X10,mult(X11,mult(X11,X11)))].
% 2.75/3.17  [48=param(6,42),[],
% 2.75/3.17  			rd(mult(X10,X11),mult(X11,X11)) 	= rd(X10,X11)].
% 2.75/3.17  [50=param(42,18),[2,5],
% 2.75/3.17  			mult(X10,mult(X11,X11)) 	= rd(X10,mult(X11,X11))].
% 2.75/3.17  [51=demod(25),[50],
% 2.75/3.17  			rd(unit,rd(X10,mult(X10,X10))) 	= X10].
% 2.75/3.17  [52=demod(16),[50],
% 2.75/3.17  			ld(X10,unit) 	= rd(X10,mult(X10,X10))].
% 2.75/3.17  [56=demod(41),[50],
% 2.75/3.17  			rd(rd(X10,mult(X11,X11)),X11) 	= mult(X10,X11)].
% 2.75/3.17  [60=demod(35),[50],
% 2.75/3.17  			rd(rd(X10,mult(X11,X11)),mult(X11,X10)) 	= X11].
% 2.75/3.17  [61=demod(22),[50],
% 2.75/3.17  			mult(rd(X10,mult(X11,X11)),X12) 	= mult(X10,mult(X11,mult(X11,X12)))].
% 2.75/3.17  [62=demod(21),[-56,48,50],
% 2.75/3.17  			rd(rd(X10,X11),X11) 	= rd(X10,mult(X11,X11))].
% 2.75/3.17  [63=demod(52),[-62,26],
% 2.75/3.17  			ld(X10,unit) 	= rd(unit,X10)].
% 2.75/3.17  [64=demod(51),[-62,26],
% 2.75/3.17  			rd(unit,rd(unit,X10)) 	= X10].
% 2.75/3.17  [65=demod(32),[-62],
% 2.75/3.17  			mult(X10,X10) 	= rd(rd(unit,X10),X10)].
% 2.75/3.17  [66=demod(33),[65],
% 2.75/3.17  			rd(mult(X10,mult(X10,X11)),X11) 	= rd(rd(unit,X10),X10)].
% 2.75/3.17  [68=demod(30),[65],
% 2.75/3.17  			rd(mult(X10,mult(X10,X11)),rd(rd(unit,X10),X10)) 	= X11].
% 2.75/3.17  [69=demod(28),[65,65],
% 2.75/3.17  			ld(rd(rd(unit,X10),X10),X11) 	= rd(X11,rd(rd(unit,X10),X10))].
% 2.75/3.17  [70=demod(18),[65],
% 2.75/3.17  			mult(rd(rd(unit,X10),X10),X11) 	= mult(X10,mult(X10,X11))].
% 2.75/3.17  [71=demod(62),[65],
% 2.75/3.17  			rd(rd(X10,X11),X11) 	= rd(X10,rd(rd(unit,X11),X11))].
% 2.75/3.17  [72=demod(61),[65],
% 2.75/3.17  			mult(rd(X10,rd(rd(unit,X11),X11)),X12) 	= mult(X10,mult(X11,mult(X11,X12)))].
% 2.75/3.17  [73=demod(60),[65],
% 2.75/3.17  			rd(rd(X10,rd(rd(unit,X11),X11)),mult(X11,X10)) 	= X11].
% 2.75/3.17  [76=demod(56),[65],
% 2.75/3.17  			mult(X10,X11) 	= rd(rd(X10,rd(rd(unit,X11),X11)),X11)].
% 2.75/3.17  [77=demod(8),[76],
% 2.75/3.17  			ld(X10,rd(rd(X10,rd(rd(unit,X11),X11)),X11)) 	= X11].
% 2.75/3.17  [80=demod(65),[76],
% 2.75/3.17  			rd(rd(X10,rd(rd(unit,X10),X10)),X10) 	= rd(rd(unit,X10),X10)].
% 2.75/3.17  [81=demod(68),[76,76],
% 2.75/3.17  			rd(rd(rd(X10,rd(rd(unit,rd(rd(X10,rd(rd(unit,X11),X11)),X11)),rd(rd(X10,rd(rd(unit,X11),X11)),X11))),rd(rd(X10,rd(rd(unit,X11),X11)),X11)),rd(rd(unit,X10),X10)) 	= X11].
% 2.75/3.17  [82=demod(66),[76,76],
% 2.75/3.17  			rd(rd(rd(X10,rd(rd(unit,rd(rd(X10,rd(rd(unit,X11),X11)),X11)),rd(rd(X10,rd(rd(unit,X11),X11)),X11))),rd(rd(X10,rd(rd(unit,X11),X11)),X11)),X11) 	= rd(rd(unit,X10),X10)].
% 2.75/3.17  [85=demod(73),[76],
% 2.75/3.17  			rd(rd(X10,rd(rd(unit,X11),X11)),rd(rd(X11,rd(rd(unit,X10),X10)),X10)) 	= X11].
% 2.75/3.17  [88=demod(70),[76,76,76],
% 2.75/3.17  			rd(rd(rd(rd(unit,X10),X10),rd(rd(unit,X11),X11)),X11) 	= rd(rd(X10,rd(rd(unit,rd(rd(X10,rd(rd(unit,X11),X11)),X11)),rd(rd(X10,rd(rd(unit,X11),X11)),X11))),rd(rd(X10,rd(rd(unit,X11),X11)),X11))].
% 2.75/3.17  [91=demod(72),[76,76,76,76],
% 2.75/3.17  			rd(rd(rd(X10,rd(rd(unit,X11),X11)),rd(rd(unit,X12),X12)),X12) 	= rd(rd(X10,rd(rd(unit,rd(rd(X11,rd(rd(unit,rd(rd(X11,rd(rd(unit,X12),X12)),X12)),rd(rd(X11,rd(rd(unit,X12),X12)),X12))),rd(rd(X11,rd(rd(unit,X12),X12)),X12))),rd(rd(X11,rd(rd(unit,rd(rd(X11,rd(rd(unit,X12),X12)),X12)),rd(rd(X11,rd(rd(unit,X12),X12)),X12))),rd(rd(X11,rd(rd(unit,X12),X12)),X12)))),rd(rd(X11,rd(rd(unit,rd(rd(X11,rd(rd(unit,X12),X12)),X12)),rd(rd(X11,rd(rd(unit,X12),X12)),X12))),rd(rd(X11,rd(rd(unit,X12),X12)),X12)))].
% 2.75/3.17  [93=demod(48),[76,76,80],
% 2.75/3.17  			rd(rd(rd(X10,rd(rd(unit,X11),X11)),X11),rd(rd(unit,X11),X11)) 	= rd(X10,X11)].
% 2.75/3.17  [97=demod(38),[76,76,80,76,-71,26,23,76,80,76,-71,26,23,76],
% 2.75/3.17  			rd(rd(rd(X10,rd(rd(unit,X11),X11)),X11),rd(rd(unit,X10),X10)) 	= rd(rd(X10,rd(rd(unit,rd(X11,rd(rd(unit,X10),X10))),rd(X11,rd(rd(unit,X10),X10)))),rd(X11,rd(rd(unit,X10),X10)))].
% 2.75/3.17  [98=demod(81),[97],
% 2.75/3.17  			rd(rd(X10,rd(rd(unit,rd(rd(rd(X10,rd(rd(unit,X11),X11)),X11),rd(rd(unit,X10),X10))),rd(rd(rd(X10,rd(rd(unit,X11),X11)),X11),rd(rd(unit,X10),X10)))),rd(rd(rd(X10,rd(rd(unit,X11),X11)),X11),rd(rd(unit,X10),X10))) 	= X11].
% 2.75/3.17  [99=demod(37),[76,80,76,-71,26,23,76],
% 2.75/3.17  			ld(X10,rd(X11,rd(rd(unit,X10),X10))) 	= rd(rd(X10,rd(rd(unit,X11),X11)),X11)].
% 2.75/3.17  [100=demod(19),[76,76,76,80,76,-71,26,23],
% 2.75/3.17  			rd(rd(X10,rd(rd(unit,rd(rd(X10,rd(rd(unit,X11),X11)),X11)),rd(rd(X10,rd(rd(unit,X11),X11)),X11))),rd(rd(X10,rd(rd(unit,X11),X11)),X11)) 	= rd(X11,rd(rd(unit,X10),X10))].
% 2.75/3.17  [101=demod(88),[100],
% 2.75/3.17  			rd(rd(rd(rd(unit,X10),X10),rd(rd(unit,X11),X11)),X11) 	= rd(X11,rd(rd(unit,X10),X10))].
% 2.75/3.17  [103=demod(82),[100],
% 2.75/3.17  			rd(rd(X10,rd(rd(unit,X11),X11)),X10) 	= rd(rd(unit,X11),X11)].
% 2.75/3.17  [104=demod(91),[100,100,100],
% 2.75/3.17  			rd(rd(rd(X10,rd(rd(unit,X11),X11)),rd(rd(unit,X12),X12)),X12) 	= rd(rd(X10,rd(rd(unit,rd(X12,rd(rd(unit,X11),X11))),rd(X12,rd(rd(unit,X11),X11)))),rd(X12,rd(rd(unit,X11),X11)))].
% 2.75/3.17  [105=demod(98),[-104],
% 2.75/3.17  			rd(rd(rd(X10,rd(rd(unit,X10),X10)),rd(rd(unit,rd(rd(X10,rd(rd(unit,X11),X11)),X11)),rd(rd(X10,rd(rd(unit,X11),X11)),X11))),rd(rd(X10,rd(rd(unit,X11),X11)),X11)) 	= X11].
% 2.75/3.17  [108=demod(47),[76,76,103,76,-71,26,23,93,76,103,76,-71,26,23,76],
% 2.75/3.17  			rd(rd(X10,rd(rd(unit,rd(X11,rd(rd(unit,X11),X11))),rd(X11,rd(rd(unit,X11),X11)))),rd(X11,rd(rd(unit,X11),X11))) 	= rd(X10,X11)].
% 2.75/3.17  [112=demod(42),[76,103,76,-71,26,23,76],
% 2.75/3.17  			rd(rd(X10,rd(rd(unit,X11),X11)),X11) 	= rd(rd(X10,X11),rd(rd(unit,X11),X11))].
% 2.75/3.17  [114=demod(101),[112],
% 2.75/3.17  			rd(rd(rd(rd(unit,X10),X10),X11),rd(rd(unit,X11),X11)) 	= rd(X11,rd(rd(unit,X10),X10))].
% 2.75/3.17  [116=demod(99),[112],
% 2.75/3.17  			ld(X10,rd(X11,rd(rd(unit,X10),X10))) 	= rd(rd(X10,X11),rd(rd(unit,X11),X11))].
% 2.75/3.17  [117=demod(77),[112],
% 2.75/3.17  			ld(X10,rd(rd(X10,X11),rd(rd(unit,X11),X11))) 	= X11].
% 2.75/3.17  [118=demod(76),[112],
% 2.75/3.17  			mult(X10,X11) 	= rd(rd(X10,X11),rd(rd(unit,X11),X11))].
% 2.75/3.17  [120=demod(100),[112,112,112,112],
% 2.75/3.17  			rd(rd(X10,rd(rd(X10,X11),rd(rd(unit,X11),X11))),rd(rd(unit,rd(rd(X10,X11),rd(rd(unit,X11),X11))),rd(rd(X10,X11),rd(rd(unit,X11),X11)))) 	= rd(X11,rd(rd(unit,X10),X10))].
% 2.75/3.17  [122=demod(108),[112],
% 2.75/3.17  			rd(rd(X10,rd(X11,rd(rd(unit,X11),X11))),rd(rd(unit,rd(X11,rd(rd(unit,X11),X11))),rd(X11,rd(rd(unit,X11),X11)))) 	= rd(X10,X11)].
% 2.75/3.17  [123=demod(85),[112],
% 2.75/3.17  			rd(rd(X10,rd(rd(unit,X11),X11)),rd(rd(X11,X10),rd(rd(unit,X10),X10))) 	= X11].
% 2.75/3.17  [125=demod(105),[112,112,112,112],
% 2.75/3.17  			rd(rd(rd(X10,rd(rd(unit,X10),X10)),rd(rd(X10,X11),rd(rd(unit,X11),X11))),rd(rd(unit,rd(rd(X10,X11),rd(rd(unit,X11),X11))),rd(rd(X10,X11),rd(rd(unit,X11),X11)))) 	= X11].
% 2.75/3.17  [127=param(69,24),[],
% 2.75/3.17  			rd(rd(unit,X10),rd(rd(unit,X10),X10)) 	= X10].
% 2.75/3.17  [131=param(71,26),[],
% 2.75/3.17  			rd(X10,rd(rd(unit,X10),X10)) 	= rd(unit,X10)].
% 2.75/3.17  [132=demod(125),[131],
% 2.75/3.17  			rd(rd(rd(unit,X10),rd(rd(X10,X11),rd(rd(unit,X11),X11))),rd(rd(unit,rd(rd(X10,X11),rd(rd(unit,X11),X11))),rd(rd(X10,X11),rd(rd(unit,X11),X11)))) 	= X11].
% 2.75/3.17  [133=demod(122),[131,131,64,131],
% 2.75/3.17  			rd(rd(X10,rd(unit,X11)),rd(X11,rd(unit,X11))) 	= rd(X10,X11)].
% 2.75/3.17  [135=param(71,64),[64],
% 2.75/3.17  			rd(unit,rd(X10,rd(unit,X10))) 	= rd(X10,rd(unit,X10))].
% 2.75/3.17  [140=param(103,127),[],
% 2.75/3.17  			rd(rd(unit,X10),X10) 	= rd(X10,rd(unit,X10))].
% 2.75/3.17  [143=demod(118),[140],
% 2.75/3.17  			mult(X10,X11) 	= rd(rd(X10,X11),rd(X11,rd(unit,X11)))].
% 2.75/3.17  [144=demod(117),[140],
% 2.75/3.17  			ld(X10,rd(rd(X10,X11),rd(X11,rd(unit,X11)))) 	= X11].
% 2.75/3.17  [146=demod(112),[140,140],
% 2.75/3.17  			rd(rd(X10,rd(X11,rd(unit,X11))),X11) 	= rd(rd(X10,X11),rd(X11,rd(unit,X11)))].
% 2.75/3.17  [148=demod(71),[140],
% 2.75/3.17  			rd(rd(X10,X11),X11) 	= rd(X10,rd(X11,rd(unit,X11)))].
% 2.75/3.17  [149=demod(123),[148,135,148,135],
% 2.75/3.17  			rd(rd(X10,rd(X11,rd(unit,X11))),rd(rd(X11,X10),rd(X10,rd(unit,X10)))) 	= X11].
% 2.75/3.17  [150=demod(116),[148,135,148,135],
% 2.75/3.17  			ld(X10,rd(X11,rd(X10,rd(unit,X10)))) 	= rd(rd(X10,X11),rd(X11,rd(unit,X11)))].
% 2.75/3.17  [151=demod(114),[148,135,148,135,148,135],
% 2.75/3.17  			rd(rd(rd(X10,rd(unit,X10)),X11),rd(X11,rd(unit,X11))) 	= rd(X11,rd(X10,rd(unit,X10)))].
% 2.75/3.17  [155=demod(132),[148,135,148,135,148,135,148,135],
% 2.75/3.17  			rd(rd(rd(unit,X10),rd(rd(X10,X11),rd(X11,rd(unit,X11)))),rd(rd(rd(X10,X11),rd(X11,rd(unit,X11))),rd(unit,rd(rd(X10,X11),rd(X11,rd(unit,X11)))))) 	= X11].
% 2.75/3.17  [156=demod(120),[148,135,148,135,148,135,148,135,148,135],
% 2.75/3.17  			rd(rd(X10,rd(rd(X10,X11),rd(X11,rd(unit,X11)))),rd(rd(rd(X10,X11),rd(X11,rd(unit,X11))),rd(unit,rd(rd(X10,X11),rd(X11,rd(unit,X11)))))) 	= rd(X11,rd(X10,rd(unit,X10)))].
% 2.75/3.17  [162=param(133,27),[63,63,64,148,135,63],
% 2.75/3.17  			rd(rd(X10,X11),rd(X11,rd(unit,X11))) 	= rd(X10,rd(unit,X11))].
% 2.75/3.17  [163=demod(149),[162],
% 2.75/3.17  			rd(rd(X10,rd(X11,rd(unit,X11))),rd(X11,rd(unit,X10))) 	= X11].
% 2.75/3.17  [166=demod(151),[162],
% 2.75/3.17  			rd(rd(X10,rd(unit,X10)),rd(unit,X11)) 	= rd(X11,rd(X10,rd(unit,X10)))].
% 2.75/3.17  [170=demod(156),[162,162,162,162],
% 2.75/3.17  			rd(X10,rd(unit,rd(X10,rd(unit,X11)))) 	= rd(X11,rd(X10,rd(unit,X10)))].
% 2.75/3.17  [171=demod(162),[],
% 2.75/3.17  			rd(rd(X10,X11),rd(X11,rd(unit,X11))) 	= rd(X10,rd(unit,X11))].
% 2.75/3.17  [172=demod(133),[],
% 2.75/3.17  			rd(rd(X10,rd(unit,X11)),rd(X11,rd(unit,X11))) 	= rd(X10,X11)].
% 2.75/3.17  [173=demod(155),[171,171,171,171],
% 2.75/3.17  			rd(rd(unit,X10),rd(unit,rd(X10,rd(unit,X11)))) 	= X11].
% 2.75/3.17  [175=demod(150),[171],
% 2.75/3.17  			ld(X10,rd(X11,rd(X10,rd(unit,X10)))) 	= rd(X10,rd(unit,X11))].
% 2.75/3.17  [176=demod(146),[171],
% 2.75/3.17  			rd(rd(X10,rd(X11,rd(unit,X11))),X11) 	= rd(X10,rd(unit,X11))].
% 2.75/3.17  [177=demod(144),[171],
% 2.75/3.17  			ld(X10,rd(X10,rd(unit,X11))) 	= X11].
% 2.75/3.17  [178=demod(143),[171],
% 2.75/3.17  			mult(X10,X11) 	= rd(X10,rd(unit,X11))].
% 2.75/3.17  [179=param(11,178),[178,178,178],
% 2.75/3.17  			thtop(rd(rd(a,rd(unit,b)),rd(unit,a)),rd(a,rd(unit,rd(b,rd(unit,a))))) 	= thmtrue].
% 2.75/3.17  [180=param(177,27),[63],
% 2.75/3.17  			ld(X10,rd(X10,X11)) 	= rd(unit,X11)].
% 2.75/3.17  [184=param(148,176),[148,135,26,23],
% 2.75/3.17  			rd(rd(X10,rd(unit,X11)),X11) 	= X10].
% 2.75/3.17  [185=param(184,27),[63],
% 2.75/3.17  			rd(rd(X10,X11),rd(unit,X11)) 	= X10].
% 2.75/3.17  [187=param(163,27),[63],
% 2.75/3.17  			rd(rd(rd(unit,X10),rd(X11,rd(unit,X11))),rd(X11,X10)) 	= X11].
% 2.75/3.17  [189=param(163,184),[135],
% 2.75/3.17  			rd(X10,rd(X11,rd(unit,rd(X10,rd(X11,rd(unit,X11)))))) 	= X11].
% 2.75/3.17  [192=param(175,184),[135],
% 2.75/3.17  			ld(X10,X11) 	= rd(X10,rd(unit,rd(X11,rd(X10,rd(unit,X10)))))].
% 2.75/3.17  [193=demod(180),[192],
% 2.75/3.17  			rd(X10,rd(unit,rd(rd(X10,X11),rd(X10,rd(unit,X10))))) 	= rd(unit,X11)].
% 2.75/3.17  [202=param(173,64),[],
% 2.75/3.17  			rd(rd(unit,X10),rd(unit,rd(X10,X11))) 	= rd(unit,X11)].
% 2.75/3.17  [203=param(202,64),[],
% 2.75/3.17  			rd(X10,rd(unit,rd(rd(unit,X10),X11))) 	= rd(unit,X11)].
% 2.75/3.17  [205=param(184,202),[],
% 2.75/3.17  			rd(rd(unit,X10),rd(X11,X10)) 	= rd(unit,X11)].
% 2.75/3.17  [207=param(205,64),[],
% 2.75/3.17  			rd(X10,rd(X11,rd(unit,X10))) 	= rd(unit,X11)].
% 2.75/3.17  [208=param(202,205),[64,64],
% 2.75/3.17  			rd(X10,X11) 	= rd(unit,rd(X11,X10))].
% 2.75/3.17  [209=demod(148),[208],
% 2.75/3.17  			rd(unit,rd(X10,rd(X11,X10))) 	= rd(X11,rd(X10,rd(unit,X10)))].
% 2.75/3.17  [210=demod(172),[],
% 2.75/3.17  			rd(rd(X10,rd(unit,X11)),rd(X11,rd(unit,X11))) 	= rd(X10,X11)].
% 2.75/3.17  [211=demod(171),[],
% 2.75/3.17  			rd(rd(X10,X11),rd(X11,rd(unit,X11))) 	= rd(X10,rd(unit,X11))].
% 2.75/3.17  [213=demod(193),[],
% 2.75/3.17  			rd(X10,rd(unit,rd(rd(X10,X11),rd(X10,rd(unit,X10))))) 	= rd(unit,X11)].
% 2.75/3.17  [216=demod(184),[208],
% 2.75/3.17  			rd(unit,rd(X10,rd(X11,rd(unit,X10)))) 	= X11].
% 2.75/3.17  [219=param(202,208),[],
% 2.75/3.17  			rd(rd(X10,X11),rd(unit,rd(rd(X11,X10),X12))) 	= rd(unit,X12)].
% 2.75/3.17  [220=param(205,208),[],
% 2.75/3.17  			rd(rd(X10,X11),rd(X12,rd(X11,X10))) 	= rd(unit,X12)].
% 2.75/3.17  [228=param(208,220),[64],
% 2.75/3.17  			rd(rd(X10,rd(X11,X12)),rd(X12,X11)) 	= X10].
% 2.75/3.17  [232=param(185,228),[],
% 2.75/3.17  			rd(X10,rd(unit,rd(X11,X12))) 	= rd(X10,rd(X12,X11))].
% 2.75/3.17  [233=param(228,187),[],
% 2.75/3.17  			rd(X10,rd(X11,X10)) 	= rd(rd(unit,X11),rd(X10,rd(unit,X10)))].
% 2.75/3.17  [234=param(228,207),[23],
% 2.75/3.17  			rd(rd(X10,X11),rd(X12,rd(X11,rd(unit,X12)))) 	= X10].
% 2.75/3.17  [235=param(189,208),[],
% 2.75/3.17  			rd(X10,rd(X11,rd(rd(X11,rd(unit,X11)),X10))) 	= X11].
% 2.75/3.17  [236=param(235,166),[],
% 2.75/3.17  			rd(rd(unit,X10),rd(X11,rd(X10,rd(X11,rd(unit,X11))))) 	= X11].
% 2.75/3.17  [238=param(234,208),[],
% 2.75/3.17  			rd(rd(unit,rd(X10,X11)),rd(X12,rd(X10,rd(unit,X12)))) 	= X11].
% 2.75/3.17  [241=param(211,208),[-233,208],
% 2.75/3.17  			rd(X10,rd(unit,rd(X10,rd(X10,X11)))) 	= rd(X11,rd(unit,X10))].
% 2.75/3.17  [243=demod(185),[-241],
% 2.75/3.17  			rd(X10,rd(unit,rd(X10,rd(X10,rd(X11,X10))))) 	= X11].
% 2.75/3.17  [246=param(243,208),[],
% 2.75/3.17  			rd(X10,rd(unit,rd(X10,rd(X10,rd(unit,rd(X10,X11)))))) 	= X11].
% 2.75/3.17  [247=param(228,243),[23],
% 2.75/3.17  			rd(X10,rd(X11,rd(X11,rd(X10,X11)))) 	= X11].
% 2.75/3.17  [248=param(247,208),[],
% 2.75/3.17  			rd(X10,rd(X11,rd(X11,rd(unit,rd(X11,X10))))) 	= X11].
% 2.75/3.17  [250=param(248,207),[64],
% 2.75/3.17  			rd(rd(X10,rd(unit,X11)),rd(X11,rd(X11,X10))) 	= X11].
% 2.75/3.17  [252=param(208,250),[],
% 2.75/3.17  			rd(rd(X10,rd(X10,X11)),rd(X11,rd(unit,X10))) 	= rd(unit,X10)].
% 2.75/3.17  [256=param(232,208),[],
% 2.75/3.17  			rd(X10,rd(unit,rd(X11,X12))) 	= rd(unit,rd(rd(X12,X11),X10))].
% 2.75/3.17  [259=param(228,252),[],
% 2.75/3.17  			rd(rd(unit,X10),rd(rd(unit,X10),X11)) 	= rd(X10,rd(X10,X11))].
% 2.75/3.17  [260=param(202,219),[64,64],
% 2.75/3.17  			rd(rd(unit,rd(X10,X11)),X12) 	= rd(rd(X11,X10),X12)].
% 2.75/3.17  [261=param(208,209),[23],
% 2.75/3.17  			rd(unit,rd(X10,rd(X11,rd(unit,X11)))) 	= rd(X11,rd(X10,X11))].
% 2.75/3.17  [262=demod(213),[261,208],
% 2.75/3.17  			rd(X10,rd(X10,rd(unit,rd(X10,rd(X10,X11))))) 	= rd(unit,X11)].
% 2.75/3.17  [267=param(208,209),[64],
% 2.75/3.17  			rd(X10,rd(X11,X10)) 	= rd(rd(X10,rd(unit,X10)),X11)].
% 2.75/3.17  [269=param(267,208),[],
% 2.75/3.17  			rd(rd(X10,rd(unit,X10)),X11) 	= rd(X10,rd(unit,rd(X10,X11)))].
% 2.75/3.17  [270=param(163,210),[],
% 2.75/3.17  			rd(rd(X10,X11),rd(X11,rd(unit,rd(X10,rd(unit,X11))))) 	= X11].
% 2.75/3.17  [284=param(236,210),[],
% 2.75/3.17  			rd(rd(unit,rd(X10,rd(unit,X11))),rd(X11,rd(X10,X11))) 	= X11].
% 2.75/3.17  [287=param(284,260),[],
% 2.75/3.17  			rd(rd(rd(unit,X10),X11),rd(X10,rd(X11,X10))) 	= X10].
% 2.75/3.17  [288=param(208,287),[],
% 2.75/3.17  			rd(rd(X10,rd(X11,X10)),rd(rd(unit,X10),X11)) 	= rd(unit,X10)].
% 2.75/3.17  [290=param(238,207),[64],
% 2.75/3.17  			rd(X10,rd(X11,rd(X12,rd(unit,X11)))) 	= rd(X10,rd(unit,X12))].
% 2.75/3.17  [291=param(238,259),[64],
% 2.75/3.17  			rd(rd(X11,X10),rd(rd(X11,X10),rd(X11,rd(X11,X10)))) 	= X10].
% 2.75/3.17  [292=param(228,288),[],
% 2.75/3.17  			rd(rd(unit,X10),rd(X11,rd(unit,X10))) 	= rd(X10,rd(X11,X10))].
% 2.75/3.17  [308=param(208,269),[],
% 2.75/3.17  			rd(unit,rd(X10,rd(unit,rd(X10,X11)))) 	= rd(X11,rd(X10,rd(unit,X10)))].
% 2.75/3.17  [310=demod(210),[],
% 2.75/3.17  			rd(rd(X10,rd(unit,X11)),rd(X11,rd(unit,X11))) 	= rd(X10,X11)].
% 2.75/3.17  [311=demod(211),[],
% 2.75/3.17  			rd(rd(X10,X11),rd(X11,rd(unit,X11))) 	= rd(X10,rd(unit,X11))].
% 2.75/3.17  [323=param(311,208),[269],
% 2.75/3.17  			rd(X10,rd(unit,X11)) 	= rd(unit,rd(X11,rd(unit,rd(X11,rd(X10,X11)))))].
% 2.75/3.17  [324=param(208,311),[269],
% 2.75/3.17  			rd(unit,rd(X10,rd(unit,X11))) 	= rd(X11,rd(unit,rd(X11,rd(X10,X11))))].
% 2.75/3.17  [331=param(292,220),[23,23],
% 2.75/3.17  			rd(rd(X10,X11),rd(rd(X11,X10),rd(X10,X11))) 	= rd(unit,rd(X10,X11))].
% 2.75/3.17  [340=param(203,170),[64,135],
% 2.75/3.17  			rd(X10,rd(unit,rd(X11,rd(unit,rd(X11,X10))))) 	= rd(X11,rd(unit,X11))].
% 2.75/3.17  [344=param(259,202),[],
% 2.75/3.17  			rd(rd(unit,X10),rd(unit,X11)) 	= rd(X10,rd(X10,rd(unit,rd(X10,X11))))].
% 2.75/3.17  [349=demod(291),[],
% 2.75/3.17  			rd(rd(X10,X11),rd(rd(X10,X11),rd(X10,rd(X10,X11)))) 	= X11].
% 2.75/3.17  [350=param(203,259),[],
% 2.75/3.17  			rd(unit,rd(rd(unit,X10),X11)) 	= rd(X10,rd(unit,rd(X10,rd(X10,X11))))].
% 2.75/3.17  [352=demod(228),[],
% 2.75/3.17  			rd(rd(X10,rd(X11,X12)),rd(X12,X11)) 	= X10].
% 2.75/3.17  [356=param(208,350),[23],
% 2.75/3.17  			rd(rd(unit,X10),X11) 	= rd(unit,rd(X10,rd(unit,rd(X10,rd(X10,X11)))))].
% 2.75/3.17  [382=demod(344),[356],
% 2.75/3.17  			rd(unit,rd(X10,rd(unit,rd(X10,rd(X10,rd(unit,X11)))))) 	= rd(X10,rd(X10,rd(unit,rd(X10,X11))))].
% 2.75/3.17  [409=param(352,209),[23],
% 2.75/3.17  			rd(rd(X10,rd(X11,rd(X12,X11))),rd(X12,rd(X11,rd(unit,X11)))) 	= X10].
% 2.75/3.17  [410=param(248,209),[64,269],
% 2.75/3.17  			rd(X10,rd(unit,rd(X10,rd(X11,rd(X11,rd(X10,rd(X11,X10))))))) 	= X11].
% 2.75/3.17  [412=param(219,209),[64,135],
% 2.75/3.17  			rd(rd(X10,X11),rd(X12,rd(rd(X11,X10),X12))) 	= rd(X12,rd(unit,X12))].
% 2.75/3.17  [417=param(234,349),[207],
% 2.75/3.17  			rd(X10,rd(unit,rd(rd(X11,X10),rd(X11,rd(X11,X10))))) 	= rd(X11,X10)].
% 2.75/3.17  [418=param(340,207),[64],
% 2.75/3.17  			rd(rd(X10,rd(unit,X11)),rd(unit,rd(X11,X10))) 	= rd(X11,rd(unit,X11))].
% 2.75/3.17  [422=param(219,331),[64],
% 2.75/3.17  			rd(unit,rd(rd(X10,X11),rd(X11,X10))) 	= rd(rd(X10,X11),rd(X11,X10))].
% 2.75/3.17  [434=param(208,290),[],
% 2.75/3.17  			rd(unit,rd(X10,rd(unit,X11))) 	= rd(rd(X12,rd(X11,rd(unit,X12))),X10)].
% 2.75/3.17  [439=param(417,209),[],
% 2.75/3.17  			rd(X10,rd(X11,rd(rd(X11,X10),rd(unit,rd(X11,X10))))) 	= rd(X11,X10)].
% 2.75/3.17  [442=param(439,256),[422],
% 2.75/3.17  			rd(X10,rd(X11,rd(rd(X10,X11),rd(X11,X10)))) 	= rd(X11,X10)].
% 2.75/3.17  [449=param(246,410),[],
% 2.75/3.17  			rd(X10,rd(unit,rd(X10,X11))) 	= rd(X11,rd(X11,rd(X10,rd(X11,X10))))].
% 2.75/3.17  [457=param(449,208),[64],
% 2.75/3.17  			rd(X11,rd(X11,rd(X10,rd(X11,X10)))) 	= rd(X10,rd(X11,X10))].
% 2.75/3.17  [461=param(270,434),[],
% 2.75/3.17  			rd(rd(X10,X11),rd(X11,rd(rd(X12,rd(X11,rd(unit,X12))),X10))) 	= X11].
% 2.75/3.17  [462=param(461,412),[208,216,208,356,409,208,457,64,208,64],
% 2.75/3.17  			rd(rd(X10,rd(X11,X10)),rd(X11,rd(X10,rd(X11,X10)))) 	= X11].
% 2.75/3.17  [464=param(234,462),[207],
% 2.75/3.17  			rd(X10,rd(unit,rd(X10,rd(X11,rd(X10,X11))))) 	= rd(X11,rd(X10,X11))].
% 2.75/3.17  [468=param(179,207),[323,208,382,-208],
% 2.75/3.17  			thtop(rd(unit,rd(a,rd(a,rd(a,rd(b,a))))),rd(a,rd(unit,rd(b,rd(X10,rd(a,rd(unit,X10))))))) 	= thmtrue].
% 2.75/3.17  [471=param(269,64),[208,135,269,356,64,356,262],
% 2.75/3.17  			rd(unit,rd(X10,rd(unit,rd(X10,rd(unit,X11))))) 	= rd(X10,rd(unit,rd(X10,X11)))].
% 2.75/3.17  [500=demod(310),[],
% 2.75/3.17  			rd(rd(X10,rd(unit,X11)),rd(X11,rd(unit,X11))) 	= rd(X10,X11)].
% 2.75/3.17  [510=param(262,457),[464],
% 2.75/3.17  			rd(unit,rd(X10,rd(X11,rd(X10,X11)))) 	= rd(X10,rd(X11,rd(X10,X11)))].
% 2.75/3.17  [520=param(418,457),[323,208,457,471,510,457],
% 2.75/3.17  			rd(rd(X10,rd(X11,X10)),rd(unit,rd(X10,rd(X11,X10)))) 	= rd(X11,rd(unit,X11))].
% 2.75/3.17  [523=param(207,209),[],
% 2.75/3.17  			rd(rd(X10,rd(X11,X10)),rd(X12,rd(X11,rd(X10,rd(unit,X10))))) 	= rd(unit,X12)].
% 2.75/3.17  [570=param(442,261),[208,356,523,23,23,520,135],
% 2.75/3.17  			rd(rd(X10,X11),rd(X11,rd(X10,rd(unit,X10)))) 	= rd(X11,rd(X10,X11))].
% 2.75/3.17  [590=param(270,308),[570],
% 2.75/3.17  			rd(rd(X10,rd(X10,X11)),rd(X11,rd(X10,X11))) 	= rd(X10,X11)].
% 2.75/3.17  [596=param(352,590),[208],
% 2.75/3.17  			rd(rd(X10,X11),rd(unit,rd(X11,rd(X10,X11)))) 	= rd(X10,rd(X10,X11))].
% 2.75/3.17  [599=param(596,209),[],
% 2.75/3.17  			rd(rd(X10,X11),rd(X10,rd(X11,rd(unit,X11)))) 	= rd(X10,rd(X10,X11))].
% 2.75/3.17  [607=param(599,500),[208,216,208,216,208],
% 2.75/3.17  			rd(unit,rd(X10,rd(X10,rd(unit,X11)))) 	= rd(X10,rd(X10,X11))].
% 2.75/3.17  [608=demod(246),[607],
% 2.75/3.17  			rd(X10,rd(X10,rd(X10,rd(X10,X11)))) 	= X11].
% 2.75/3.17  [612=demod(382),[607],
% 2.75/3.17  			rd(unit,rd(X10,rd(X10,rd(X10,X11)))) 	= rd(X10,rd(X10,rd(unit,rd(X10,X11))))].
% 2.75/3.17  [634=param(468,608),[612,209,64,208,323,208,-323,216,324,209,10],
% 2.75/3.17  			thmtrue 	= thmfalse].
% 2.75/3.17  % SZS output end CNFRefutation
% 2.75/3.17  Space:  18029 KB 
%------------------------------------------------------------------------------