= repository_nav ontology.repository, :ontologies

= ontology_nav ontology, :theorems

%h3

= t('proof_attempts.show.head')

= link_to resource.theorem, locid_for(resource.theorem, :proof_attempts)

= render partial: 'theorems/proof_status', locals: {proof_status: resource.proof_status}

%div.timestamp= resource.updated_at

= render partial: '/shared/state', locals: {resource: resource}

= render partial: 'configuration', locals: {configuration: resource.proof_attempt_configuration}

- if resource.state == 'done'

%h4= t('proof_attempts.show.time_taken')

= resource.time_taken

= t('proof_attempts.show.seconds')

%h4= t('proof_attempts.show.used_axioms')

- if resource.used_axioms.empty?

= t('proof_attempts.show.no_used_axioms')

- else

= render partial: 'sentences_list', locals: {sentences: resource.used_axioms}

%h4= t('proof_attempts.show.used_theorems')

- if resource.used_theorems.empty?

= t('proof_attempts.show.no_used_theorems')

- else

= render partial: 'sentences_list', locals: {sentences: resource.used_theorems}

%h4= t('proof_attempts.show.generated_axioms')

- if resource.generated_axioms.empty?

= t('proof_attempts.show.no_generated_axioms')

- else

%ul.sentences-list

- resource.generated_axioms.each do |axiom|

%li= axiom

%h4= t('proof_attempts.show.prover')

= resource.prover

%h4= t('proof_attempts.show.tactic_script')

%pre= resource.tactic_script

%h4= t('proof_attempts.show.prover_output')

- if resource.prover_output

= link_to t('proof_attempts.show.prover_output'), locid_for(resource.prover_output)

- else

= t('proof_attempts.show.no_prover_output')