The cow is blue. The cow is cold. The cow is young. If the cow is young and the cow is cold then the cow is green. If someone is blue then they are rough. Young people are blue. If the cow is rough and the cow is green then the cow is young. If someone is rough and cold then they are young. All young, green people are rough. If someone is blue and green then they are cold. If someone is rough and young then they are blue.
The cow is blue.
("cow" "is" "blue" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is young.
("cow" "is" "young" "+")
If the cow is young and the cow is cold then the cow is green.
((("cow" "is" "young" "+") ("cow" "is" "cold" "+")) -> ("cow" "is" "green" "+"))
If someone is blue then they are rough.
((("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
Young people are blue.
((("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
If the cow is rough and the cow is green then the cow is young.
((("cow" "is" "rough" "+") ("cow" "is" "green" "+")) -> ("cow" "is" "young" "+"))
If someone is rough and cold then they are young.
((("someone" "is" "rough" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
All young, green people are rough.
((("someone" "is" "young" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
If someone is blue and green then they are cold.
((("someone" "is" "blue" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
If someone is rough and young then they are blue.
((("someone" "is" "rough" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
The cow is cold.
True
1
proof
[(triple2)]
("cow" "is" "cold" "+")
triple2
The cow is not blue.
False
1
inv-proof
[(triple1 OR ((triple3) -> rule3) OR ((((triple3 ((triple3 triple2) -> rule1)) -> rule6) triple3) -> rule8))]
("cow" "is" "blue" "-")
triple1
((triple3) -> (rule3 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
((((triple3 ((triple3 triple2) -> (rule1 % int3))) -> (rule6 % int2)) triple3) -> (rule8 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow is green.
("cow" "is" "green" "+")
int3
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 chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
@0: The cow is blue.[(triple1 OR ((triple3) -> rule3) OR ((((triple3 ((triple3 triple2) -> rule1)) -> rule6) triple3) -> rule8))] The cow is cold.[(triple2)] The cow is young.[(triple3 OR ((((triple1) -> rule2) triple2) -> rule5))] @1: The cow is green.[(((triple3 triple2) -> rule1) OR ((((((triple1) -> rule2) triple2) -> rule5) triple2) -> rule1))] The cow is rough.[(((triple1) -> rule2) OR ((((triple3) -> rule3)) -> rule2) OR ((triple3 ((triple3 triple2) -> rule1)) -> rule6))]
The cow is blue.
("cow" "is" "blue" "+")
triple1
((triple3) -> (rule3 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
((((triple3 ((triple3 triple2) -> (rule1 % int3))) -> (rule6 % int2)) triple3) -> (rule8 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow is green.
("cow" "is" "green" "+")
int3
The cow is cold.
("cow" "is" "cold" "+")
triple2
The cow is young.
("cow" "is" "young" "+")
triple3
((((triple1) -> (rule2 % int2)) triple2) -> (rule5 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow is green.
("cow" "is" "green" "+")
((triple3 triple2) -> (rule1 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
((((((triple1) -> (rule2 % int3)) triple2) -> (rule5 % int2)) triple2) -> (rule1 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
int3
The cow is rough.
("cow" "is" "rough" "+")
((triple1) -> (rule2 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
((triple3 ((triple3 triple2) -> (rule1 % int2))) -> (rule6 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2