The cow is big. The cow is green. The cow is red. The cow is round. The cow is young. If something is big and round then it is red. All big, red things are green. If the cow is green and the cow is young then the cow is red. Green things are red. Green things are round. All round things are red.
The cow is big.
("cow" "is" "big" "+")
The cow is green.
("cow" "is" "green" "+")
The cow is red.
("cow" "is" "red" "+")
The cow is round.
("cow" "is" "round" "+")
The cow is young.
("cow" "is" "young" "+")
If something is big and round then it is red.
((("something" "is" "big" "+") ("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
All big, red things are green.
((("something" "is" "big" "+") ("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
If the cow is green and the cow is young then the cow is red.
((("cow" "is" "green" "+") ("cow" "is" "young" "+")) -> ("cow" "is" "red" "+"))
Green things are red.
((("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
Green things are round.
((("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
All round things are red.
((("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
The cow is big.
True
1
proof
[(triple1)]
("cow" "is" "big" "+")
triple1
The cow is not round.
False
1
inv-proof
[(triple4 OR ((triple2) -> rule5) OR ((((triple1 triple3) -> rule2)) -> rule5))]
("cow" "is" "round" "-")
triple4
((triple2) -> (rule5 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
((((triple1 triple3) -> (rule2 % int2))) -> (rule5 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow does not eat the cow.
Unknown
inv-random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "-")
The cow chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
@0: The cow is big.[(triple1)] The cow is green.[(triple2 OR ((triple1 triple3) -> rule2) OR ((triple1 ((triple4) -> rule6)) -> rule2) OR ((triple1 ((triple1 triple4) -> rule1)) -> rule2))] The cow is red.[(triple3 OR ((triple2) -> rule4) OR ((triple4) -> rule6) OR ((triple1 triple4) -> rule1) OR ((triple2 triple5) -> rule3) OR ((((triple2) -> rule5)) -> rule6) OR ((triple1 ((triple2) -> rule5)) -> rule1))] The cow is round.[(triple4 OR ((triple2) -> rule5) OR ((((triple1 triple3) -> rule2)) -> rule5))] The cow is young.[(triple5)]
The cow is big.
("cow" "is" "big" "+")
triple1
The cow is green.
("cow" "is" "green" "+")
triple2
((triple1 triple3) -> (rule2 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
((triple1 ((triple4) -> (rule6 % int2))) -> (rule2 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
((triple1 ((triple1 triple4) -> (rule1 % int2))) -> (rule2 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow is red.
("cow" "is" "red" "+")
triple3
((triple2) -> (rule4 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
((triple4) -> (rule6 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
((triple1 triple4) -> (rule1 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
((triple2 triple5) -> (rule3 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
((triple1 ((triple2) -> (rule5 % int2))) -> (rule1 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
The cow is round.
("cow" "is" "round" "+")
triple4
((triple2) -> (rule5 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
((((triple1 triple3) -> (rule2 % int2))) -> (rule5 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow is young.
("cow" "is" "young" "+")
triple5