The cow is blue. The cow is rough. The cow is young. Cold people are rough. If someone is young then they are cold. Rough, young people are cold. If the cow is blue then the cow is cold. If the cow is blue then the cow is cold. If someone is rough and cold then they are young. If someone is cold and blue then they are red. If someone is blue and not young then they are red.
The cow is blue.
("cow" "is" "blue" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow is young.
("cow" "is" "young" "+")
Cold people are rough.
((("someone" "is" "cold" "+")) -> ("someone" "is" "rough" "+"))
If someone is young then they are cold.
((("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
Rough, young people are cold.
((("someone" "is" "rough" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
If the cow is blue then the cow is cold.
((("cow" "is" "blue" "+")) -> ("cow" "is" "cold" "+"))
If the cow is blue then the cow is cold.
((("cow" "is" "blue" "+")) -> ("cow" "is" "cold" "+"))
If someone is rough and cold then they are young.
((("someone" "is" "rough" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
If someone is cold and blue then they are red.
((("someone" "is" "cold" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
If someone is blue and not young then they are red.
((("someone" "is" "blue" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "red" "+"))
The cow is rough.
True
1
proof
[(triple2 OR ((((triple1) -> rule4)) -> rule1) OR ((((triple1) -> rule5)) -> rule1) OR ((((triple3) -> rule2)) -> rule1))]
("cow" "is" "rough" "+")
triple2
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow is not rough.
False
1
inv-proof
[(triple2 OR ((((triple1) -> rule4)) -> rule1) OR ((((triple1) -> rule5)) -> rule1) OR ((((triple3) -> rule2)) -> rule1))]
("cow" "is" "rough" "-")
triple2
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow is cold.
True
2
proof
[(((triple1) -> rule4) OR ((triple1) -> rule5) OR ((triple3) -> rule2) OR ((triple2 triple3) -> rule3))]
("cow" "is" "cold" "+")
((triple1) -> (rule4 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
((triple1) -> (rule5 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
((triple3) -> (rule2 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
((triple2 triple3) -> (rule3 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is not cold.
False
2
inv-proof
[(((triple1) -> rule4) OR ((triple1) -> rule5) OR ((triple3) -> rule2) OR ((triple2 triple3) -> rule3))]
("cow" "is" "cold" "-")
((triple1) -> (rule4 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
((triple1) -> (rule5 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
((triple3) -> (rule2 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
((triple2 triple3) -> (rule3 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is red.
True
4
proof
[(((((triple1) -> rule4) triple1) -> rule7) OR ((((triple1) -> rule5) triple1) -> rule7) OR ((((triple3) -> rule2) triple1) -> rule7) OR ((((triple2 triple3) -> rule3) triple1) -> rule7))]
("cow" "is" "red" "+")
((((triple1) -> (rule4 % int2)) triple1) -> (rule7 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
((((triple1) -> (rule5 % int2)) triple1) -> (rule7 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
((((triple3) -> (rule2 % int2)) triple1) -> (rule7 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
((((triple2 triple3) -> (rule3 % int2)) triple1) -> (rule7 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow is not red.
False
4
inv-proof
[(((((triple1) -> rule4) triple1) -> rule7) OR ((((triple1) -> rule5) triple1) -> rule7) OR ((((triple3) -> rule2) triple1) -> rule7) OR ((((triple2 triple3) -> rule3) triple1) -> rule7))]
("cow" "is" "red" "-")
((((triple1) -> (rule4 % int2)) triple1) -> (rule7 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
((((triple1) -> (rule5 % int2)) triple1) -> (rule7 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
((((triple3) -> (rule2 % int2)) triple1) -> (rule7 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
((((triple2 triple3) -> (rule3 % int2)) triple1) -> (rule7 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow does not need the cow.
Unknown
inv-random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "-")
The cow visits the cow.
Unknown
random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "+")
@0: The cow is blue.[(triple1)] The cow is rough.[(triple2 OR ((((triple1) -> rule4)) -> rule1) OR ((((triple1) -> rule5)) -> rule1) OR ((((triple3) -> rule2)) -> rule1))] The cow is young.[(triple3 OR ((triple2 ((triple1) -> rule4)) -> rule6) OR ((triple2 ((triple1) -> rule5)) -> rule6) OR ((((((triple1) -> rule4)) -> rule1) ((triple1) -> rule4)) -> rule6) OR ((((((triple1) -> rule4)) -> rule1) ((triple1) -> rule5)) -> rule6) OR ((((((triple1) -> rule5)) -> rule1) ((triple1) -> rule4)) -> rule6) OR ((((((triple1) -> rule5)) -> rule1) ((triple1) -> rule5)) -> rule6))] @1: The cow is cold.[(((triple1) -> rule4) OR ((triple1) -> rule5) OR ((triple3) -> rule2) OR ((triple2 triple3) -> rule3))] @2: The cow is red.[(((((triple1) -> rule4) triple1) -> rule7) OR ((((triple1) -> rule5) triple1) -> rule7) OR ((((triple3) -> rule2) triple1) -> rule7) OR ((((triple2 triple3) -> rule3) triple1) -> rule7))]
The cow is blue.
("cow" "is" "blue" "+")
triple1
The cow is rough.
("cow" "is" "rough" "+")
triple2
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow is young.
("cow" "is" "young" "+")
triple3
((triple2 ((triple1) -> (rule4 % int2))) -> (rule6 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
((triple2 ((triple1) -> (rule5 % int2))) -> (rule6 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
((((((triple1) -> (rule4 % int3))) -> (rule1 % int2)) ((triple1) -> (rule4 % int3))) -> (rule6 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
((((((triple1) -> (rule4 % int3))) -> (rule1 % int2)) ((triple1) -> (rule5 % int3))) -> (rule6 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
((((((triple1) -> (rule5 % int3))) -> (rule1 % int2)) ((triple1) -> (rule4 % int3))) -> (rule6 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
((((((triple1) -> (rule5 % int3))) -> (rule1 % int2)) ((triple1) -> (rule5 % int3))) -> (rule6 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The cow is cold.
("cow" "is" "cold" "+")
((triple1) -> (rule4 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
((triple1) -> (rule5 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
((triple3) -> (rule2 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
((triple2 triple3) -> (rule3 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is red.
("cow" "is" "red" "+")
((((triple1) -> (rule4 % int2)) triple1) -> (rule7 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
((((triple1) -> (rule5 % int2)) triple1) -> (rule7 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
((((triple3) -> (rule2 % int2)) triple1) -> (rule7 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
((((triple2 triple3) -> (rule3 % int2)) triple1) -> (rule7 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2