%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SWV235+1 : TPTP v8.1.0. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n024.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 : Wed Jul 20 19:49:58 EDT 2022
% Result : Theorem 234.68s 226.66s
% Output : Proof 234.77s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : SWV235+1 : TPTP v8.1.0. Released v3.2.0.
% 0.04/0.14 % Command : leancop_casc.sh %s %d
% 0.14/0.35 % Computer : n024.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 600
% 0.14/0.35 % DateTime : Tue Jun 14 19:48:48 EDT 2022
% 0.14/0.35 % CPUTime :
% 234.68/226.66 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 234.68/226.67 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 234.77/226.68
% 234.77/226.68 %-----------------------------------------------------
% 234.77/226.68 fof(encrypt_data, axiom, ! [_42315, _42318] : (p(_42315) & p(crypt(xor(km, data), _42318)) => p(crypt(_42318, _42315))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', encrypt_data)).
% 234.77/226.68 fof(decrypt_knowledge, axiom, ! [_42516, _42519] : (p(crypt(_42516, _42519)) & p(_42516) => p(_42519)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', decrypt_knowledge)).
% 234.77/226.68 fof(initial_knowledge_of_intruder_7, axiom, p(crypt(xor(km, imp), xor(rand, xor(imp, exp)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', initial_knowledge_of_intruder_7)).
% 234.77/226.68 fof(an_account_number, axiom, p(a), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', an_account_number)).
% 234.77/226.68 fof(key_part_import___part_3, axiom, ! [_42810, _42813, _42816] : (p(_42810) & p(crypt(xor(km, xor(_42813, kp)), _42816)) & p(_42813) => p(crypt(xor(km, _42813), xor(_42816, _42810)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', key_part_import___part_3)).
% 234.77/226.68 fof(key_export, axiom, ! [_43092, _43095, _43098] : (p(crypt(xor(km, _43092), _43095)) & p(_43092) & p(crypt(xor(km, exp), _43098)) => p(crypt(xor(_43098, _43092), _43095))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', key_export)).
% 234.77/226.68 fof(combine_with_XOR, axiom, ! [_43373, _43376] : (p(_43373) & p(_43376) => p(xor(_43373, _43376))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', combine_with_XOR)).
% 234.77/226.68 fof(initial_knowledge_of_intruder_11, axiom, p(exp), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', initial_knowledge_of_intruder_11)).
% 234.77/226.68 fof(initial_knowledge_of_intruder_5, axiom, p(pin), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', initial_knowledge_of_intruder_5)).
% 234.77/226.68 fof(key_part_import___part_2, axiom, ! [_43639, _43642, _43645] : (p(_43639) & p(crypt(xor(km, xor(kp, _43642)), _43645)) & p(_43642) => p(crypt(xor(km, xor(_43642, kp)), xor(_43639, _43645)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', key_part_import___part_2)).
% 234.77/226.68 fof(key_part_import___part_1, axiom, ! [_43936, _43939] : (p(_43936) & p(_43939) => p(crypt(xor(km, xor(kp, _43939)), _43936))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', key_part_import___part_1)).
% 234.77/226.68 fof(key_import, axiom, ! [_44138, _44141, _44144, _44147, _44150] : (p(crypt(xor(_44138, _44141), _44144)) & p(_44147) & p(crypt(xor(km, imp), _44150)) => p(crypt(xor(km, _44147), decrypt(xor(_44150, _44147), crypt(xor(_44138, _44141), _44144))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', key_import)).
% 234.77/226.68 fof(initial_knowledge_of_intruder_6, axiom, p(crypt(xor(km, pin), pp)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', initial_knowledge_of_intruder_6)).
% 234.77/226.68 fof(find_pin, conjecture, p(crypt(pp, a)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', find_pin)).
% 234.77/226.68 fof(initial_knowledge_of_intruder_3, axiom, p(data), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', initial_knowledge_of_intruder_3)).
% 234.77/226.68 fof(encrypt_knowledge, axiom, ! [_44679, _44682] : (p(_44682) & p(_44679) => p(crypt(_44679, _44682))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', encrypt_knowledge)).
% 234.77/226.68
% 234.77/226.68 cnf(1, plain, [-(p(crypt(_20513, _20459))), p(_20459), p(crypt(xor(km, data), _20513))], clausify(encrypt_data)).
% 234.77/226.68 cnf(2, plain, [-(p(_23113)), p(crypt(_23062, _23113)), p(_23062)], clausify(decrypt_knowledge)).
% 234.77/226.68 cnf(3, plain, [-(p(crypt(xor(km, imp), xor(rand, xor(imp, exp)))))], clausify(initial_knowledge_of_intruder_7)).
% 234.77/226.68 cnf(4, plain, [-(p(a))], clausify(an_account_number)).
% 234.77/226.68 cnf(5, plain, [-(p(crypt(xor(km, _19796), xor(_19871, _19720)))), p(_19720), p(crypt(xor(km, xor(_19796, kp)), _19871)), p(_19796)], clausify(key_part_import___part_3)).
% 234.77/226.68 cnf(6, plain, [-(p(crypt(xor(_17894, _17749), _17822))), p(crypt(xor(km, _17749), _17822)), p(_17749), p(crypt(xor(km, exp), _17894))], clausify(key_export)).
% 234.77/226.68 cnf(7, plain, [-(p(xor(_22692, _22743))), p(_22692), p(_22743)], clausify(combine_with_XOR)).
% 234.77/226.68 cnf(8, plain, [-(p(exp))], clausify(initial_knowledge_of_intruder_11)).
% 234.77/226.68 cnf(9, plain, [-(p(pin))], clausify(initial_knowledge_of_intruder_5)).
% 234.77/226.68 cnf(10, plain, [-(p(crypt(xor(km, xor(_19014, kp)), xor(_18935, _19092)))), p(_18935), p(crypt(xor(km, xor(kp, _19014)), _19092)), p(_19014)], clausify(key_part_import___part_2)).
% 234.77/226.68 cnf(11, plain, [-(p(crypt(xor(km, xor(kp, _18536)), _18479))), p(_18479), p(_18536)], clausify(key_part_import___part_1)).
% 234.77/226.68 cnf(12, plain, [-(p(crypt(xor(km, _16890), decrypt(xor(_16982, _16890), crypt(xor(_16608, _16703), _16797))))), p(crypt(xor(_16608, _16703), _16797)), p(_16890), p(crypt(xor(km, imp), _16982))], clausify(key_import)).
% 234.77/226.68 cnf(13, plain, [-(p(crypt(xor(km, pin), pp)))], clausify(initial_knowledge_of_intruder_6)).
% 234.77/226.68 cnf(14, plain, [p(crypt(pp, a))], clausify(find_pin)).
% 234.77/226.68 cnf(15, plain, [-(p(data))], clausify(initial_knowledge_of_intruder_3)).
% 234.77/226.68 cnf(16, plain, [-(p(crypt(_23432, _23483))), p(_23483), p(_23432)], clausify(encrypt_knowledge)).
% 234.77/226.68
% 234.77/226.68 cnf('1',plain,[p(crypt(pp, a))],start(14)).
% 234.77/226.68 cnf('1.1',plain,[-(p(crypt(pp, a))), p(a), p(pp)],extension(16,bind([[_23483, _23432], [a, pp]]))).
% 234.77/226.68 cnf('1.1.1',plain,[-(p(a))],extension(4)).
% 234.77/226.68 cnf('1.1.2',plain,[-(p(pp)), p(crypt(xor(xor(xor(crypt(xor(km, imp), xor(rand, xor(imp, exp))), crypt(xor(km, imp), xor(rand, xor(imp, exp)))), crypt(decrypt(xor(xor(rand, xor(imp, exp)), data), crypt(xor(km, imp), xor(rand, xor(imp, exp)))), crypt(xor(km, imp), xor(rand, xor(imp, exp))))), pin), pp)), p(xor(xor(xor(crypt(xor(km, imp), xor(rand, xor(imp, exp))), crypt(xor(km, imp), xor(rand, xor(imp, exp)))), crypt(decrypt(xor(xor(rand, xor(imp, exp)), data), crypt(xor(km, imp), xor(rand, xor(imp, exp)))), crypt(xor(km, imp), xor(rand, xor(imp, exp))))), pin))],extension(2,bind([[_23113, _23062], [pp, xor(xor(xor(crypt(xor(km, imp), xor(rand, xor(imp, exp))), crypt(xor(km, imp), xor(rand, xor(imp, exp)))), crypt(decrypt(xor(xor(rand, xor(imp, exp)), data), crypt(xor(km, imp), xor(rand, xor(imp, exp)))), crypt(xor(km, imp), xor(rand, xor(imp, exp))))), pin)]]))).
% 234.77/226.68 cnf('1.1.2.1',plain,[-(p(crypt(xor(xor(xor(crypt(xor(km, imp), xor(rand, xor(imp, exp))), crypt(xor(km, imp), xor(rand, xor(imp, exp)))), crypt(decrypt(xor(xor(rand, xor(imp, exp)), data), crypt(xor(km, imp), xor(rand, xor(imp, exp)))), crypt(xor(km, imp), xor(rand, xor(imp, exp))))), pin), pp))), p(crypt(xor(km, pin), pp)), p(pin), p(crypt(xor(km, exp), xor(xor(crypt(xor(km, imp), xor(rand, xor(imp, exp))), crypt(xor(km, imp), xor(rand, xor(imp, exp)))), crypt(decrypt(xor(xor(rand, xor(imp, exp)), data), crypt(xor(km, imp), xor(rand, xor(imp, exp)))), crypt(xor(km, imp), xor(rand, xor(imp, exp)))))))],extension(6,bind([[_17822, _17749, _17894], [pp, pin, xor(xor(crypt(xor(km, imp), xor(rand, xor(imp, exp))), crypt(xor(km, imp), xor(rand, xor(imp, exp)))), crypt(decrypt(xor(xor(rand, xor(imp, exp)), data), crypt(xor(km, imp), xor(rand, xor(imp, exp)))), crypt(xor(km, imp), xor(rand, xor(imp, exp)))))]]))).
% 234.77/226.68 cnf('1.1.2.1.1',plain,[-(p(crypt(xor(km, pin), pp)))],extension(13)).
% 234.77/226.68 cnf('1.1.2.1.2',plain,[-(p(pin))],extension(9)).
% 234.77/226.68 cnf('1.1.2.1.3',plain,[-(p(crypt(xor(km, exp), xor(xor(crypt(xor(km, imp), xor(rand, xor(imp, exp))), crypt(xor(km, imp), xor(rand, xor(imp, exp)))), crypt(decrypt(xor(xor(rand, xor(imp, exp)), data), crypt(xor(km, imp), xor(rand, xor(imp, exp)))), crypt(xor(km, imp), xor(rand, xor(imp, exp)))))))), p(crypt(decrypt(xor(xor(rand, xor(imp, exp)), data), crypt(xor(km, imp), xor(rand, xor(imp, exp)))), crypt(xor(km, imp), xor(rand, xor(imp, exp))))), p(crypt(xor(km, xor(exp, kp)), xor(crypt(xor(km, imp), xor(rand, xor(imp, exp))), crypt(xor(km, imp), xor(rand, xor(imp, exp)))))), p(exp)],extension(5,bind([[_19720, _19871, _19796], [crypt(decrypt(xor(xor(rand, xor(imp, exp)), data), crypt(xor(km, imp), xor(rand, xor(imp, exp)))), crypt(xor(km, imp), xor(rand, xor(imp, exp)))), xor(crypt(xor(km, imp), xor(rand, xor(imp, exp))), crypt(xor(km, imp), xor(rand, xor(imp, exp)))), exp]]))).
% 234.77/226.68 cnf('1.1.2.1.3.1',plain,[-(p(crypt(decrypt(xor(xor(rand, xor(imp, exp)), data), crypt(xor(km, imp), xor(rand, xor(imp, exp)))), crypt(xor(km, imp), xor(rand, xor(imp, exp)))))), p(crypt(xor(km, imp), xor(rand, xor(imp, exp)))), p(crypt(xor(km, data), decrypt(xor(xor(rand, xor(imp, exp)), data), crypt(xor(km, imp), xor(rand, xor(imp, exp))))))],extension(1,bind([[_20459, _20513], [crypt(xor(km, imp), xor(rand, xor(imp, exp))), decrypt(xor(xor(rand, xor(imp, exp)), data), crypt(xor(km, imp), xor(rand, xor(imp, exp))))]]))).
% 234.77/226.68 cnf('1.1.2.1.3.1.1',plain,[-(p(crypt(xor(km, imp), xor(rand, xor(imp, exp)))))],extension(3)).
% 234.77/226.68 cnf('1.1.2.1.3.1.2',plain,[-(p(crypt(xor(km, data), decrypt(xor(xor(rand, xor(imp, exp)), data), crypt(xor(km, imp), xor(rand, xor(imp, exp))))))), p(crypt(xor(km, imp), xor(rand, xor(imp, exp)))), p(data), p(crypt(xor(km, imp), xor(rand, xor(imp, exp))))],extension(12,bind([[_16608, _16703, _16797, _16890, _16982], [km, imp, xor(rand, xor(imp, exp)), data, xor(rand, xor(imp, exp))]]))).
% 234.77/226.68 cnf('1.1.2.1.3.1.2.1',plain,[-(p(crypt(xor(km, imp), xor(rand, xor(imp, exp)))))],extension(3)).
% 234.77/226.68 cnf('1.1.2.1.3.1.2.2',plain,[-(p(data))],extension(15)).
% 234.77/226.68 cnf('1.1.2.1.3.1.2.3',plain,[-(p(crypt(xor(km, imp), xor(rand, xor(imp, exp)))))],extension(3)).
% 234.77/226.68 cnf('1.1.2.1.3.2',plain,[-(p(crypt(xor(km, xor(exp, kp)), xor(crypt(xor(km, imp), xor(rand, xor(imp, exp))), crypt(xor(km, imp), xor(rand, xor(imp, exp))))))), p(crypt(xor(km, imp), xor(rand, xor(imp, exp)))), p(crypt(xor(km, xor(kp, exp)), crypt(xor(km, imp), xor(rand, xor(imp, exp))))), p(exp)],extension(10,bind([[_18935, _19092, _19014], [crypt(xor(km, imp), xor(rand, xor(imp, exp))), crypt(xor(km, imp), xor(rand, xor(imp, exp))), exp]]))).
% 234.77/226.68 cnf('1.1.2.1.3.2.1',plain,[-(p(crypt(xor(km, imp), xor(rand, xor(imp, exp)))))],extension(3)).
% 234.77/226.68 cnf('1.1.2.1.3.2.2',plain,[-(p(crypt(xor(km, xor(kp, exp)), crypt(xor(km, imp), xor(rand, xor(imp, exp)))))), p(crypt(xor(km, imp), xor(rand, xor(imp, exp)))), p(exp)],extension(11,bind([[_18479, _18536], [crypt(xor(km, imp), xor(rand, xor(imp, exp))), exp]]))).
% 234.77/226.68 cnf('1.1.2.1.3.2.2.1',plain,[-(p(crypt(xor(km, imp), xor(rand, xor(imp, exp)))))],extension(3)).
% 234.77/226.68 cnf('1.1.2.1.3.2.2.2',plain,[-(p(exp))],extension(8)).
% 234.77/226.68 cnf('1.1.2.1.3.2.3',plain,[-(p(exp))],extension(8)).
% 234.77/226.68 cnf('1.1.2.1.3.3',plain,[-(p(exp))],extension(8)).
% 234.77/226.68 cnf('1.1.2.2',plain,[-(p(xor(xor(xor(crypt(xor(km, imp), xor(rand, xor(imp, exp))), crypt(xor(km, imp), xor(rand, xor(imp, exp)))), crypt(decrypt(xor(xor(rand, xor(imp, exp)), data), crypt(xor(km, imp), xor(rand, xor(imp, exp)))), crypt(xor(km, imp), xor(rand, xor(imp, exp))))), pin))), p(xor(xor(crypt(xor(km, imp), xor(rand, xor(imp, exp))), crypt(xor(km, imp), xor(rand, xor(imp, exp)))), crypt(decrypt(xor(xor(rand, xor(imp, exp)), data), crypt(xor(km, imp), xor(rand, xor(imp, exp)))), crypt(xor(km, imp), xor(rand, xor(imp, exp)))))), p(pin)],extension(7,bind([[_22692, _22743], [xor(xor(crypt(xor(km, imp), xor(rand, xor(imp, exp))), crypt(xor(km, imp), xor(rand, xor(imp, exp)))), crypt(decrypt(xor(xor(rand, xor(imp, exp)), data), crypt(xor(km, imp), xor(rand, xor(imp, exp)))), crypt(xor(km, imp), xor(rand, xor(imp, exp))))), pin]]))).
% 234.77/226.68 cnf('1.1.2.2.1',plain,[-(p(xor(xor(crypt(xor(km, imp), xor(rand, xor(imp, exp))), crypt(xor(km, imp), xor(rand, xor(imp, exp)))), crypt(decrypt(xor(xor(rand, xor(imp, exp)), data), crypt(xor(km, imp), xor(rand, xor(imp, exp)))), crypt(xor(km, imp), xor(rand, xor(imp, exp))))))), p(xor(crypt(xor(km, imp), xor(rand, xor(imp, exp))), crypt(xor(km, imp), xor(rand, xor(imp, exp))))), p(crypt(decrypt(xor(xor(rand, xor(imp, exp)), data), crypt(xor(km, imp), xor(rand, xor(imp, exp)))), crypt(xor(km, imp), xor(rand, xor(imp, exp)))))],extension(7,bind([[_22692, _22743], [xor(crypt(xor(km, imp), xor(rand, xor(imp, exp))), crypt(xor(km, imp), xor(rand, xor(imp, exp)))), crypt(decrypt(xor(xor(rand, xor(imp, exp)), data), crypt(xor(km, imp), xor(rand, xor(imp, exp)))), crypt(xor(km, imp), xor(rand, xor(imp, exp))))]]))).
% 234.77/226.68 cnf('1.1.2.2.1.1',plain,[-(p(xor(crypt(xor(km, imp), xor(rand, xor(imp, exp))), crypt(xor(km, imp), xor(rand, xor(imp, exp)))))), p(crypt(xor(km, imp), xor(rand, xor(imp, exp)))), p(crypt(xor(km, imp), xor(rand, xor(imp, exp))))],extension(7,bind([[_22692, _22743], [crypt(xor(km, imp), xor(rand, xor(imp, exp))), crypt(xor(km, imp), xor(rand, xor(imp, exp)))]]))).
% 234.77/226.68 cnf('1.1.2.2.1.1.1',plain,[-(p(crypt(xor(km, imp), xor(rand, xor(imp, exp)))))],extension(3)).
% 234.77/226.68 cnf('1.1.2.2.1.1.2',plain,[-(p(crypt(xor(km, imp), xor(rand, xor(imp, exp)))))],extension(3)).
% 234.77/226.68 cnf('1.1.2.2.1.2',plain,[-(p(crypt(decrypt(xor(xor(rand, xor(imp, exp)), data), crypt(xor(km, imp), xor(rand, xor(imp, exp)))), crypt(xor(km, imp), xor(rand, xor(imp, exp)))))), p(crypt(xor(km, imp), xor(rand, xor(imp, exp)))), p(crypt(xor(km, data), decrypt(xor(xor(rand, xor(imp, exp)), data), crypt(xor(km, imp), xor(rand, xor(imp, exp))))))],extension(1,bind([[_20459, _20513], [crypt(xor(km, imp), xor(rand, xor(imp, exp))), decrypt(xor(xor(rand, xor(imp, exp)), data), crypt(xor(km, imp), xor(rand, xor(imp, exp))))]]))).
% 234.77/226.68 cnf('1.1.2.2.1.2.1',plain,[-(p(crypt(xor(km, imp), xor(rand, xor(imp, exp)))))],extension(3)).
% 234.77/226.68 cnf('1.1.2.2.1.2.2',plain,[-(p(crypt(xor(km, data), decrypt(xor(xor(rand, xor(imp, exp)), data), crypt(xor(km, imp), xor(rand, xor(imp, exp))))))), p(crypt(xor(km, imp), xor(rand, xor(imp, exp)))), p(data), p(crypt(xor(km, imp), xor(rand, xor(imp, exp))))],extension(12,bind([[_16608, _16703, _16797, _16890, _16982], [km, imp, xor(rand, xor(imp, exp)), data, xor(rand, xor(imp, exp))]]))).
% 234.77/226.68 cnf('1.1.2.2.1.2.2.1',plain,[-(p(crypt(xor(km, imp), xor(rand, xor(imp, exp)))))],extension(3)).
% 234.77/226.68 cnf('1.1.2.2.1.2.2.2',plain,[-(p(data))],extension(15)).
% 234.77/226.68 cnf('1.1.2.2.1.2.2.3',plain,[-(p(crypt(xor(km, imp), xor(rand, xor(imp, exp)))))],extension(3)).
% 234.77/226.68 cnf('1.1.2.2.2',plain,[-(p(pin))],extension(9)).
% 234.77/226.68 %-----------------------------------------------------
% 234.77/226.68
% 234.77/226.68 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------