%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SET713+4 : TPTP v8.1.0. Bugfixed v2.2.1.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% 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 : Tue Jul 19 02:55:32 EDT 2022
% Result : Theorem 91.90s 88.69s
% Output : Proof 91.99s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : SET713+4 : TPTP v8.1.0. Bugfixed v2.2.1.
% 0.03/0.14 % Command : leancop_casc.sh %s %d
% 0.13/0.35 % Computer : n012.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 600
% 0.13/0.35 % DateTime : Sat Jul 9 22:14:28 EDT 2022
% 0.13/0.35 % CPUTime :
% 91.90/88.69 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 91.99/88.70 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 91.99/88.70
% 91.99/88.70 %-----------------------------------------------------
% 91.99/88.70 fof(thII04, conjecture, ! [_135302, _135305, _135308] : (maps(_135302, _135305, _135308) & one_to_one(_135302, _135305, _135308) => one_to_one(inverse_function(_135302, _135305, _135308), _135308, _135305)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', thII04)).
% 91.99/88.70 fof(maps, axiom, ! [_135638, _135641, _135644] : (maps(_135638, _135641, _135644) <=> ! [_135665] : (member(_135665, _135641) => ? [_135683] : (member(_135683, _135644) & apply(_135638, _135665, _135683))) & ! [_135665, _135716, _135719] : (member(_135665, _135641) & member(_135716, _135644) & member(_135719, _135644) => apply(_135638, _135665, _135716) & apply(_135638, _135665, _135719) => _135716 = _135719)), file('/export/starexec/sandbox/benchmark/Axioms/SET006+1.ax', maps)).
% 91.99/88.70 fof(injective, axiom, ! [_136202, _136205, _136208] : (injective(_136202, _136205, _136208) <=> ! [_136229, _136232, _136235] : (member(_136229, _136205) & member(_136232, _136205) & member(_136235, _136208) => apply(_136202, _136229, _136235) & apply(_136202, _136232, _136235) => _136229 = _136232)), file('/export/starexec/sandbox/benchmark/Axioms/SET006+1.ax', injective)).
% 91.99/88.70 fof(surjective, axiom, ! [_136631, _136634, _136637] : (surjective(_136631, _136634, _136637) <=> ! [_136658] : (member(_136658, _136637) => ? [_136676] : (member(_136676, _136634) & apply(_136631, _136676, _136658)))), file('/export/starexec/sandbox/benchmark/Axioms/SET006+1.ax', surjective)).
% 91.99/88.70 fof(one_to_one, axiom, ! [_136932, _136935, _136938] : (one_to_one(_136932, _136935, _136938) <=> injective(_136932, _136935, _136938) & surjective(_136932, _136935, _136938)), file('/export/starexec/sandbox/benchmark/Axioms/SET006+1.ax', one_to_one)).
% 91.99/88.70 fof(inverse_function, axiom, ! [_137144, _137147, _137150, _137153, _137156] : (member(_137153, _137147) & member(_137156, _137150) => (apply(_137144, _137153, _137156) <=> apply(inverse_function(_137144, _137147, _137150), _137156, _137153))), file('/export/starexec/sandbox/benchmark/Axioms/SET006+1.ax', inverse_function)).
% 91.99/88.70
% 91.99/88.70 cnf(1, plain, [-(maps(41 ^ [], 42 ^ [], 43 ^ []))], clausify(thII04)).
% 91.99/88.70 cnf(2, plain, [one_to_one(inverse_function(41 ^ [], 42 ^ [], 43 ^ []), 43 ^ [], 42 ^ [])], clausify(thII04)).
% 91.99/88.70 cnf(3, plain, [-(_23875 = _23875)], theory(equality)).
% 91.99/88.70 cnf(4, plain, [-(member(_40890, _41021)), member(_40823, _40956), _40823 = _40890, _40956 = _41021], theory(equality)).
% 91.99/88.70 cnf(5, plain, [maps(_59619, _59746, _59872), member(_60106, _59746), -(member(4 ^ [_60106, _59872, _59746, _59619], _59872))], clausify(maps)).
% 91.99/88.70 cnf(6, plain, [maps(_59619, _59746, _59872), member(_60106, _59746), -(apply(_59619, _60106, 4 ^ [_60106, _59872, _59746, _59619]))], clausify(maps)).
% 91.99/88.70 cnf(7, plain, [maps(_59619, _59746, _59872), member(_60654, _59872), member(_60567, _59872), member(_60479, _59746), -(_60567 = _60654), apply(_59619, _60479, _60567), apply(_59619, _60479, _60654)], clausify(maps)).
% 91.99/88.70 cnf(8, plain, [-(injective(_66905, _67003, _67100)), -(member(18 ^ [_67100, _67003, _66905], _67003))], clausify(injective)).
% 91.99/88.70 cnf(9, plain, [-(injective(_66905, _67003, _67100)), -(member(19 ^ [_67100, _67003, _66905], _67003))], clausify(injective)).
% 91.99/88.70 cnf(10, plain, [-(injective(_66905, _67003, _67100)), -(member(20 ^ [_67100, _67003, _66905], _67100))], clausify(injective)).
% 91.99/88.70 cnf(11, plain, [-(injective(_66905, _67003, _67100)), -(apply(_66905, 18 ^ [_67100, _67003, _66905], 20 ^ [_67100, _67003, _66905]))], clausify(injective)).
% 91.99/88.70 cnf(12, plain, [-(injective(_66905, _67003, _67100)), -(apply(_66905, 19 ^ [_67100, _67003, _66905], 20 ^ [_67100, _67003, _66905]))], clausify(injective)).
% 91.99/88.70 cnf(13, plain, [-(injective(_66905, _67003, _67100)), 18 ^ [_67100, _67003, _66905] = 19 ^ [_67100, _67003, _66905]], clausify(injective)).
% 91.99/88.70 cnf(14, plain, [-(surjective(_68196, _68270, _68343)), -(member(22 ^ [_68343, _68270, _68196], _68343))], clausify(surjective)).
% 91.99/88.70 cnf(15, plain, [-(surjective(_68196, _68270, _68343)), member(_89956, _68270), apply(_68196, _89956, 22 ^ [_68343, _68270, _68196])], clausify(surjective)).
% 91.99/88.70 cnf(16, plain, [-(one_to_one(_69007, _69066, _69124)), injective(_69007, _69066, _69124), surjective(_69007, _69066, _69124)], clausify(one_to_one)).
% 91.99/88.70 cnf(17, plain, [member(_71031, _70880), member(_70956, _70803), apply(_70725, _70956, _71031), -(apply(inverse_function(_70725, _70803, _70880), _71031, _70956))], clausify(inverse_function)).
% 91.99/88.70 cnf(18, plain, [member(_71031, _70880), member(_70956, _70803), -(apply(_70725, _70956, _71031)), apply(inverse_function(_70725, _70803, _70880), _71031, _70956)], clausify(inverse_function)).
% 91.99/88.70
% 91.99/88.70 cnf('1',plain,[one_to_one(inverse_function(41 ^ [], 42 ^ [], 43 ^ []), 43 ^ [], 42 ^ [])],start(2)).
% 91.99/88.70 cnf('1.1',plain,[-(one_to_one(inverse_function(41 ^ [], 42 ^ [], 43 ^ []), 43 ^ [], 42 ^ [])), injective(inverse_function(41 ^ [], 42 ^ [], 43 ^ []), 43 ^ [], 42 ^ []), surjective(inverse_function(41 ^ [], 42 ^ [], 43 ^ []), 43 ^ [], 42 ^ [])],extension(16,bind([[_69007, _69066, _69124], [inverse_function(41 ^ [], 42 ^ [], 43 ^ []), 43 ^ [], 42 ^ []]]))).
% 91.99/88.70 cnf('1.1.1',plain,[-(injective(inverse_function(41 ^ [], 42 ^ [], 43 ^ []), 43 ^ [], 42 ^ [])), 18 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])] = 19 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])]],extension(13,bind([[_67100, _67003, _66905], [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])]]))).
% 91.99/88.70 cnf('1.1.1.1',plain,[-(18 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])] = 19 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])]), maps(41 ^ [], 42 ^ [], 43 ^ []), member(19 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 43 ^ []), member(18 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 43 ^ []), member(20 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 42 ^ []), apply(41 ^ [], 20 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 18 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])]), apply(41 ^ [], 20 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 19 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])])],extension(7,bind([[_59872, _59746, _60567, _59619, _60479, _60654], [43 ^ [], 42 ^ [], 18 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 41 ^ [], 20 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 19 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])]]]))).
% 91.99/88.70 cnf('1.1.1.1.1',plain,[-(maps(41 ^ [], 42 ^ [], 43 ^ []))],extension(1)).
% 91.99/88.70 cnf('1.1.1.1.2',plain,[-(member(19 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 43 ^ [])), -(injective(inverse_function(41 ^ [], 42 ^ [], 43 ^ []), 43 ^ [], 42 ^ []))],extension(9,bind([[_66905, _67003, _67100], [inverse_function(41 ^ [], 42 ^ [], 43 ^ []), 43 ^ [], 42 ^ []]]))).
% 91.99/88.70 cnf('1.1.1.1.2.1',plain,[injective(inverse_function(41 ^ [], 42 ^ [], 43 ^ []), 43 ^ [], 42 ^ [])],reduction('1.1')).
% 91.99/88.70 cnf('1.1.1.1.3',plain,[-(member(18 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 43 ^ [])), member(18 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 43 ^ []), 18 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])] = 18 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 43 ^ [] = 43 ^ []],extension(4,bind([[_40823, _40890, _40956, _41021], [18 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 18 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 43 ^ [], 43 ^ []]]))).
% 91.99/88.70 cnf('1.1.1.1.3.1',plain,[-(member(18 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 43 ^ [])), -(injective(inverse_function(41 ^ [], 42 ^ [], 43 ^ []), 43 ^ [], 42 ^ []))],extension(8,bind([[_66905, _67003, _67100], [inverse_function(41 ^ [], 42 ^ [], 43 ^ []), 43 ^ [], 42 ^ []]]))).
% 91.99/88.70 cnf('1.1.1.1.3.1.1',plain,[injective(inverse_function(41 ^ [], 42 ^ [], 43 ^ []), 43 ^ [], 42 ^ [])],reduction('1.1')).
% 91.99/88.70 cnf('1.1.1.1.3.2',plain,[-(18 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])] = 18 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])])],extension(3,bind([[_23875], [18 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])]]]))).
% 91.99/88.70 cnf('1.1.1.1.3.3',plain,[-(43 ^ [] = 43 ^ [])],extension(3,bind([[_23875], [43 ^ []]]))).
% 91.99/88.70 cnf('1.1.1.1.4',plain,[-(member(20 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 42 ^ [])), -(injective(inverse_function(41 ^ [], 42 ^ [], 43 ^ []), 43 ^ [], 42 ^ []))],extension(10,bind([[_66905, _67003, _67100], [inverse_function(41 ^ [], 42 ^ [], 43 ^ []), 43 ^ [], 42 ^ []]]))).
% 91.99/88.70 cnf('1.1.1.1.4.1',plain,[injective(inverse_function(41 ^ [], 42 ^ [], 43 ^ []), 43 ^ [], 42 ^ [])],reduction('1.1')).
% 91.99/88.70 cnf('1.1.1.1.5',plain,[-(apply(41 ^ [], 20 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 18 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])])), member(18 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 43 ^ []), member(20 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 42 ^ []), apply(inverse_function(41 ^ [], 42 ^ [], 43 ^ []), 18 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 20 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])])],extension(18,bind([[_70725, _70803, _70880, _71031, _70956], [41 ^ [], 42 ^ [], 43 ^ [], 18 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 20 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])]]]))).
% 91.99/88.70 cnf('1.1.1.1.5.1',plain,[-(member(18 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 43 ^ [])), -(injective(inverse_function(41 ^ [], 42 ^ [], 43 ^ []), 43 ^ [], 42 ^ []))],extension(8,bind([[_66905, _67003, _67100], [inverse_function(41 ^ [], 42 ^ [], 43 ^ []), 43 ^ [], 42 ^ []]]))).
% 91.99/88.70 cnf('1.1.1.1.5.1.1',plain,[injective(inverse_function(41 ^ [], 42 ^ [], 43 ^ []), 43 ^ [], 42 ^ [])],reduction('1.1')).
% 91.99/88.70 cnf('1.1.1.1.5.2',plain,[-(member(20 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 42 ^ [])), -(injective(inverse_function(41 ^ [], 42 ^ [], 43 ^ []), 43 ^ [], 42 ^ []))],extension(10,bind([[_66905, _67003, _67100], [inverse_function(41 ^ [], 42 ^ [], 43 ^ []), 43 ^ [], 42 ^ []]]))).
% 91.99/88.70 cnf('1.1.1.1.5.2.1',plain,[injective(inverse_function(41 ^ [], 42 ^ [], 43 ^ []), 43 ^ [], 42 ^ [])],reduction('1.1')).
% 91.99/88.70 cnf('1.1.1.1.5.3',plain,[-(apply(inverse_function(41 ^ [], 42 ^ [], 43 ^ []), 18 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 20 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])])), -(injective(inverse_function(41 ^ [], 42 ^ [], 43 ^ []), 43 ^ [], 42 ^ []))],extension(11,bind([[_66905, _67003, _67100], [inverse_function(41 ^ [], 42 ^ [], 43 ^ []), 43 ^ [], 42 ^ []]]))).
% 91.99/88.70 cnf('1.1.1.1.5.3.1',plain,[injective(inverse_function(41 ^ [], 42 ^ [], 43 ^ []), 43 ^ [], 42 ^ [])],reduction('1.1')).
% 91.99/88.70 cnf('1.1.1.1.6',plain,[-(apply(41 ^ [], 20 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 19 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])])), member(19 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 43 ^ []), member(20 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 42 ^ []), apply(inverse_function(41 ^ [], 42 ^ [], 43 ^ []), 19 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 20 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])])],extension(18,bind([[_70725, _70803, _70880, _71031, _70956], [41 ^ [], 42 ^ [], 43 ^ [], 19 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 20 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])]]]))).
% 91.99/88.70 cnf('1.1.1.1.6.1',plain,[-(member(19 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 43 ^ [])), -(injective(inverse_function(41 ^ [], 42 ^ [], 43 ^ []), 43 ^ [], 42 ^ []))],extension(9,bind([[_66905, _67003, _67100], [inverse_function(41 ^ [], 42 ^ [], 43 ^ []), 43 ^ [], 42 ^ []]]))).
% 91.99/88.70 cnf('1.1.1.1.6.1.1',plain,[injective(inverse_function(41 ^ [], 42 ^ [], 43 ^ []), 43 ^ [], 42 ^ [])],reduction('1.1')).
% 91.99/88.70 cnf('1.1.1.1.6.2',plain,[-(member(20 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 42 ^ [])), -(injective(inverse_function(41 ^ [], 42 ^ [], 43 ^ []), 43 ^ [], 42 ^ []))],extension(10,bind([[_66905, _67003, _67100], [inverse_function(41 ^ [], 42 ^ [], 43 ^ []), 43 ^ [], 42 ^ []]]))).
% 91.99/88.70 cnf('1.1.1.1.6.2.1',plain,[injective(inverse_function(41 ^ [], 42 ^ [], 43 ^ []), 43 ^ [], 42 ^ [])],reduction('1.1')).
% 91.99/88.70 cnf('1.1.1.1.6.3',plain,[-(apply(inverse_function(41 ^ [], 42 ^ [], 43 ^ []), 19 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 20 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])])), -(injective(inverse_function(41 ^ [], 42 ^ [], 43 ^ []), 43 ^ [], 42 ^ []))],extension(12,bind([[_66905, _67003, _67100], [inverse_function(41 ^ [], 42 ^ [], 43 ^ []), 43 ^ [], 42 ^ []]]))).
% 91.99/88.70 cnf('1.1.1.1.6.3.1',plain,[injective(inverse_function(41 ^ [], 42 ^ [], 43 ^ []), 43 ^ [], 42 ^ [])],reduction('1.1')).
% 91.99/88.70 cnf('1.1.2',plain,[-(surjective(inverse_function(41 ^ [], 42 ^ [], 43 ^ []), 43 ^ [], 42 ^ [])), -(member(22 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 42 ^ []))],extension(14,bind([[_68270, _68196, _68343], [43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ []), 42 ^ []]]))).
% 91.99/88.70 cnf('1.1.2.1',plain,[member(22 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 42 ^ []), maps(41 ^ [], 42 ^ [], 43 ^ []), -(apply(41 ^ [], 22 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 4 ^ [22 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 43 ^ [], 42 ^ [], 41 ^ []]))],extension(6,bind([[_60106, _59872, _59746, _59619], [22 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 43 ^ [], 42 ^ [], 41 ^ []]]))).
% 91.99/88.70 cnf('1.1.2.1.1',plain,[-(maps(41 ^ [], 42 ^ [], 43 ^ []))],extension(1)).
% 91.99/88.70 cnf('1.1.2.1.2',plain,[apply(41 ^ [], 22 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 4 ^ [22 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 43 ^ [], 42 ^ [], 41 ^ []]), member(4 ^ [22 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 43 ^ [], 42 ^ [], 41 ^ []], 43 ^ []), member(22 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 42 ^ []), -(apply(inverse_function(41 ^ [], 42 ^ [], 43 ^ []), 4 ^ [22 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 43 ^ [], 42 ^ [], 41 ^ []], 22 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])]))],extension(17,bind([[_70725, _70803, _70880, _71031, _70956], [41 ^ [], 42 ^ [], 43 ^ [], 4 ^ [22 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 43 ^ [], 42 ^ [], 41 ^ []], 22 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])]]]))).
% 91.99/88.70 cnf('1.1.2.1.2.1',plain,[-(member(4 ^ [22 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 43 ^ [], 42 ^ [], 41 ^ []], 43 ^ [])), maps(41 ^ [], 42 ^ [], 43 ^ []), member(22 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 42 ^ [])],extension(5,bind([[_59619, _59872, _60106, _59746], [41 ^ [], 43 ^ [], 22 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 42 ^ []]]))).
% 91.99/88.70 cnf('1.1.2.1.2.1.1',plain,[-(maps(41 ^ [], 42 ^ [], 43 ^ []))],extension(1)).
% 91.99/88.70 cnf('1.1.2.1.2.1.2',plain,[-(member(22 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 42 ^ []))],reduction('1.1.2')).
% 91.99/88.70 cnf('1.1.2.1.2.2',plain,[-(member(22 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 42 ^ []))],reduction('1.1.2')).
% 91.99/88.70 cnf('1.1.2.1.2.3',plain,[apply(inverse_function(41 ^ [], 42 ^ [], 43 ^ []), 4 ^ [22 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 43 ^ [], 42 ^ [], 41 ^ []], 22 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])]), -(surjective(inverse_function(41 ^ [], 42 ^ [], 43 ^ []), 43 ^ [], 42 ^ [])), member(4 ^ [22 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 43 ^ [], 42 ^ [], 41 ^ []], 43 ^ [])],extension(15,bind([[_68196, _68343, _89956, _68270], [inverse_function(41 ^ [], 42 ^ [], 43 ^ []), 42 ^ [], 4 ^ [22 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 43 ^ [], 42 ^ [], 41 ^ []], 43 ^ []]]))).
% 91.99/88.70 cnf('1.1.2.1.2.3.1',plain,[surjective(inverse_function(41 ^ [], 42 ^ [], 43 ^ []), 43 ^ [], 42 ^ [])],reduction('1.1')).
% 91.99/88.70 cnf('1.1.2.1.2.3.2',plain,[-(member(4 ^ [22 ^ [42 ^ [], 43 ^ [], inverse_function(41 ^ [], 42 ^ [], 43 ^ [])], 43 ^ [], 42 ^ [], 41 ^ []], 43 ^ []))],lemmata('1.1.2.1.2')).
% 91.99/88.70 %-----------------------------------------------------
% 91.99/88.71
% 91.99/88.71 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------