The cow is big. The cow is blue. The cow is cold. The cow is rough. The cow is young. If something is young then it is blue. Young things are rough. All rough, cold things are blue. Rough things are big. Young, rough things are cold. Young things are cold. Big, young things are blue. If the cow is young and the cow is blue then the cow is big.
The cow is big.
("cow" "is" "big" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow is young.
("cow" "is" "young" "+")
If something is young then it is blue.
((("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
Young things are rough.
((("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
All rough, cold things are blue.
((("something" "is" "rough" "+") ("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
Rough things are big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
Young, rough things are cold.
((("something" "is" "young" "+") ("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
Young things are cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
Big, young things are blue.
((("something" "is" "big" "+") ("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
If the cow is young and the cow is blue then the cow is big.
((("cow" "is" "young" "+") ("cow" "is" "blue" "+")) -> ("cow" "is" "big" "+"))
The cow is cold.
True
1
proof
[(triple3 OR ((triple5) -> rule6) OR ((triple5 triple4) -> rule5) OR ((triple5 ((triple5) -> rule2)) -> rule5))]
("cow" "is" "cold" "+")
triple3
((triple5) -> (rule6 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
((triple5 triple4) -> (rule5 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
((triple5 ((triple5) -> (rule2 % int2))) -> (rule5 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow is not rough.
False
1
inv-proof
[(triple4 OR ((triple5) -> rule2))]
("cow" "is" "rough" "-")
triple4
((triple5) -> (rule2 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow does not chase the cow.
Unknown
inv-random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "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 big.[(triple1 OR ((triple4) -> rule4) OR ((triple5 triple2) -> rule8) OR ((((triple5) -> rule2)) -> rule4) OR ((triple5 ((triple5) -> rule1)) -> rule8) OR ((triple5 ((triple4 triple3) -> rule3)) -> rule8) OR ((triple5 ((triple4 ((triple5) -> rule6)) -> rule3)) -> rule8) OR ((triple5 ((triple4 ((triple5 triple4) -> rule5)) -> rule3)) -> rule8) OR ((triple5 ((((triple5) -> rule2) triple3) -> rule3)) -> rule8) OR ((triple5 ((((triple5) -> rule2) ((triple5) -> rule6)) -> rule3)) -> rule8) OR ((triple5 ((((triple5) -> rule2) ((triple5 triple4) -> rule5)) -> rule3)) -> rule8) OR ((triple5 ((triple4 ((triple5 ((triple5) -> rule2)) -> rule5)) -> rule3)) -> rule8) OR ((triple5 ((((triple5) -> rule2) ((triple5 ((triple5) -> rule2)) -> rule5)) -> rule3)) -> rule8))] The cow is blue.[(triple2 OR ((triple5) -> rule1) OR ((triple1 triple5) -> rule7) OR ((triple4 triple3) -> rule3) OR ((triple4 ((triple5) -> rule6)) -> rule3) OR ((triple4 ((triple5 triple4) -> rule5)) -> rule3) OR ((((triple4) -> rule4) triple5) -> rule7) OR ((((triple5) -> rule2) triple3) -> rule3) OR ((((triple5) -> rule2) ((triple5) -> rule6)) -> rule3) OR ((((triple5) -> rule2) ((triple5 triple4) -> rule5)) -> rule3) OR ((triple4 ((triple5 ((triple5) -> rule2)) -> rule5)) -> rule3) OR ((((((triple5) -> rule2)) -> rule4) triple5) -> rule7) OR ((((triple5) -> rule2) ((triple5 ((triple5) -> rule2)) -> rule5)) -> rule3))] The cow is cold.[(triple3 OR ((triple5) -> rule6) OR ((triple5 triple4) -> rule5) OR ((triple5 ((triple5) -> rule2)) -> rule5))] The cow is rough.[(triple4 OR ((triple5) -> rule2))] The cow is young.[(triple5)]
The cow is big.
("cow" "is" "big" "+")
triple1
((triple4) -> (rule4 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
((triple5 triple2) -> (rule8 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
((((triple5) -> (rule2 % int2))) -> (rule4 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
((triple5 ((triple5) -> (rule1 % int2))) -> (rule8 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
((triple5 ((triple4 triple3) -> (rule3 % int2))) -> (rule8 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
((triple5 ((triple4 ((triple5) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
((triple5 ((triple4 ((triple5 triple4) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
((triple5 ((((triple5) -> (rule2 % int3)) triple3) -> (rule3 % int2))) -> (rule8 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
int3
((triple5 ((((triple5) -> (rule2 % int4)) ((triple5) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The cow is rough.
("cow" "is" "rough" "+")
int4
((triple5 ((((triple5) -> (rule2 % int4)) ((triple5 triple4) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The cow is rough.
("cow" "is" "rough" "+")
int4
((triple5 ((triple4 ((triple5 ((triple5) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The cow is rough.
("cow" "is" "rough" "+")
int4
((triple5 ((((triple5) -> (rule2 % int4)) ((triple5 ((triple5) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The cow is rough.
("cow" "is" "rough" "+")
int4
The cow is blue.
("cow" "is" "blue" "+")
triple2
((triple5) -> (rule1 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
((triple1 triple5) -> (rule7 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
((triple4 triple3) -> (rule3 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
((triple4 ((triple5) -> (rule6 % int2))) -> (rule3 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
((triple4 ((triple5 triple4) -> (rule5 % int2))) -> (rule3 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
((((triple4) -> (rule4 % int2)) triple5) -> (rule7 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
((((triple5) -> (rule2 % int2)) triple3) -> (rule3 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
((((triple5) -> (rule2 % int3)) ((triple5) -> (rule6 % int2))) -> (rule3 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
int3
((((triple5) -> (rule2 % int3)) ((triple5 triple4) -> (rule5 % int2))) -> (rule3 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
int3
((triple4 ((triple5 ((triple5) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
int3
((((((triple5) -> (rule2 % int3))) -> (rule4 % int2)) triple5) -> (rule7 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
int3
((((triple5) -> (rule2 % int3)) ((triple5 ((triple5) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
int3
The cow is cold.
("cow" "is" "cold" "+")
triple3
((triple5) -> (rule6 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
((triple5 triple4) -> (rule5 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
((triple5 ((triple5) -> (rule2 % int2))) -> (rule5 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
triple4
((triple5) -> (rule2 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is young.
("cow" "is" "young" "+")
triple5