The cow is blue. The cow is green. The cow is rough. The cow is round. The cow is young. If someone is green and not blue then they are not young. Green people are young. All green people are young. If someone is round then they are green. If the cow is round and the cow is not blue then the cow is young. If the cow is green and the cow is not round then the cow is young.
The cow is blue.
("cow" "is" "blue" "+")
The cow is green.
("cow" "is" "green" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow is round.
("cow" "is" "round" "+")
The cow is young.
("cow" "is" "young" "+")
If someone is green and not blue then they are not young.
((("someone" "is" "green" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "young" "-"))
Green people are young.
((("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
All green people are young.
((("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
If someone is round then they are green.
((("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
If the cow is round and the cow is not blue then the cow is young.
((("cow" "is" "round" "+") ("cow" "is" "blue" "~")) -> ("cow" "is" "young" "+"))
If the cow is green and the cow is not round then the cow is young.
((("cow" "is" "green" "+") ("cow" "is" "round" "~")) -> ("cow" "is" "young" "+"))
The cow is young.
True
1
proof
[(triple5 OR ((triple2) -> rule2) OR ((triple2) -> rule3) OR ((((triple4) -> rule4)) -> rule2) OR ((((triple4) -> rule4)) -> rule3))]
("cow" "is" "young" "+")
triple5
((triple2) -> (rule2 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
((triple2) -> (rule3 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
((((triple4) -> (rule4 % int2))) -> (rule2 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
((((triple4) -> (rule4 % int2))) -> (rule3 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow is not round.
False
1
inv-proof
[(triple4)]
("cow" "is" "round" "-")
triple4
The cow does not visit the cow.
Unknown
inv-random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "-")
The cow eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
@0: The cow is blue.[(triple1)] The cow is green.[(triple2 OR ((triple4) -> rule4))] The cow is rough.[(triple3)] The cow is round.[(triple4)] The cow is young.[(triple5 OR ((triple2) -> rule2) OR ((triple2) -> rule3) OR ((((triple4) -> rule4)) -> rule2) OR ((((triple4) -> rule4)) -> rule3))]
The cow is blue.
("cow" "is" "blue" "+")
triple1
The cow is green.
("cow" "is" "green" "+")
triple2
((triple4) -> (rule4 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
triple3
The cow is round.
("cow" "is" "round" "+")
triple4
The cow is young.
("cow" "is" "young" "+")
triple5
((triple2) -> (rule2 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
((triple2) -> (rule3 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
((((triple4) -> (rule4 % int2))) -> (rule2 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
((((triple4) -> (rule4 % int2))) -> (rule3 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2