The cow is blue. The cow is rough. The cow is young. Rough, young things are blue. All blue things are round. If the cow is blue then the cow is rough. If the cow is blue and the cow is big then the cow is young. If the cow is big and the cow is blue then the cow is young. Round, big things are blue. If the cow is rough and the cow is young then the cow is blue. Young, round things are blue.
The cow is blue.
("cow" "is" "blue" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow is young.
("cow" "is" "young" "+")
Rough, young things are blue.
((("something" "is" "rough" "+") ("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
All blue things are round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
If the cow is blue then the cow is rough.
((("cow" "is" "blue" "+")) -> ("cow" "is" "rough" "+"))
If the cow is blue and the cow is big then the cow is young.
((("cow" "is" "blue" "+") ("cow" "is" "big" "+")) -> ("cow" "is" "young" "+"))
If the cow is big and the cow is blue then the cow is young.
((("cow" "is" "big" "+") ("cow" "is" "blue" "+")) -> ("cow" "is" "young" "+"))
Round, big things are blue.
((("something" "is" "round" "+") ("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
If the cow is rough and the cow is young then the cow is blue.
((("cow" "is" "rough" "+") ("cow" "is" "young" "+")) -> ("cow" "is" "blue" "+"))
Young, round things are blue.
((("something" "is" "young" "+") ("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
The cow is blue.
True
1
proof
[(triple1 OR ((triple2 triple3) -> rule1) OR ((triple2 triple3) -> rule7))]
("cow" "is" "blue" "+")
triple1
((triple2 triple3) -> (rule1 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
((triple2 triple3) -> (rule7 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is not young.
False
1
inv-proof
[(triple3)]
("cow" "is" "young" "-")
triple3
The cow is round.
True
2
proof
[(((triple1) -> rule2) OR ((((triple2 triple3) -> rule1)) -> rule2) OR ((((triple2 triple3) -> rule7)) -> rule2))]
("cow" "is" "round" "+")
((triple1) -> (rule2 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
((((triple2 triple3) -> (rule1 % int2))) -> (rule2 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
((((triple2 triple3) -> (rule7 % int2))) -> (rule2 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is not round.
False
2
inv-proof
[(((triple1) -> rule2) OR ((((triple2 triple3) -> rule1)) -> rule2) OR ((((triple2 triple3) -> rule7)) -> rule2))]
("cow" "is" "round" "-")
((triple1) -> (rule2 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
((((triple2 triple3) -> (rule1 % int2))) -> (rule2 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
((((triple2 triple3) -> (rule7 % int2))) -> (rule2 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow does not see the cow.
Unknown
inv-random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "-")
The cow chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
The cow is not big.
Unknown
inv-random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
@0: The cow is blue.[(triple1 OR ((triple2 triple3) -> rule1) OR ((triple2 triple3) -> rule7))] The cow is rough.[(triple2 OR ((triple1) -> rule3))] The cow is young.[(triple3)] @1: The cow is round.[(((triple1) -> rule2) OR ((((triple2 triple3) -> rule1)) -> rule2) OR ((((triple2 triple3) -> rule7)) -> rule2))]
The cow is blue.
("cow" "is" "blue" "+")
triple1
((triple2 triple3) -> (rule1 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
((triple2 triple3) -> (rule7 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
triple2
((triple1) -> (rule3 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is young.
("cow" "is" "young" "+")
triple3
The cow is round.
("cow" "is" "round" "+")
((triple1) -> (rule2 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
((((triple2 triple3) -> (rule1 % int2))) -> (rule2 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
((((triple2 triple3) -> (rule7 % int2))) -> (rule2 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2