The cow is big. The cow is blue. The cow is cold. The cow is nice. The cow is red. Red people are big. If the cow is red and the cow is big then the cow is cold. If someone is cold then they are red. Red, cold people are blue. If someone is big and not red then they are blue. Cold, blue people are nice.
The cow is big.
("cow" "is" "big" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow is red.
("cow" "is" "red" "+")
Red people are big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
If the cow is red and the cow is big then the cow is cold.
((("cow" "is" "red" "+") ("cow" "is" "big" "+")) -> ("cow" "is" "cold" "+"))
If someone is cold then they are red.
((("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
Red, cold people are blue.
((("someone" "is" "red" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
If someone is big and not red then they are blue.
((("someone" "is" "big" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "blue" "+"))
Cold, blue people are nice.
((("someone" "is" "cold" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
The cow is red.
True
1
proof
[(triple5 OR ((triple3) -> rule3))]
("cow" "is" "red" "+")
triple5
((triple3) -> (rule3 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is not cold.
False
1
inv-proof
[(triple3 OR ((triple5 triple1) -> rule2) OR ((triple5 ((triple5) -> rule1)) -> rule2))]
("cow" "is" "cold" "-")
triple3
((triple5 triple1) -> (rule2 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
((triple5 ((triple5) -> (rule1 % int2))) -> (rule2 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is big.
("cow" "is" "big" "+")
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 sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
@0: The cow is big.[(triple1 OR ((triple5) -> rule1) OR ((((triple3) -> rule3)) -> rule1))] The cow is blue.[(triple2 OR ((triple5 triple3) -> rule4) OR ((triple5 ((triple5 triple1) -> rule2)) -> rule4) OR ((((triple3) -> rule3) triple3) -> rule4) OR ((((triple3) -> rule3) ((triple5 triple1) -> rule2)) -> rule4) OR ((triple5 ((triple5 ((triple5) -> rule1)) -> rule2)) -> rule4) OR ((((triple3) -> rule3) ((triple5 ((triple5) -> rule1)) -> rule2)) -> rule4))] The cow is cold.[(triple3 OR ((triple5 triple1) -> rule2) OR ((triple5 ((triple5) -> rule1)) -> rule2))] The cow is nice.[(triple4 OR ((triple3 triple2) -> rule6) OR ((triple3 ((triple5 triple3) -> rule4)) -> rule6) OR ((((triple5 triple1) -> rule2) triple2) -> rule6) OR ((((triple5 triple1) -> rule2) ((triple5 triple3) -> rule4)) -> rule6) OR ((triple3 ((triple5 ((triple5 triple1) -> rule2)) -> rule4)) -> rule6) OR ((triple3 ((((triple3) -> rule3) triple3) -> rule4)) -> rule6) OR ((((triple5 ((triple5) -> rule1)) -> rule2) triple2) -> rule6) OR ((triple3 ((((triple3) -> rule3) ((triple5 triple1) -> rule2)) -> rule4)) -> rule6) OR ((((triple5 triple1) -> rule2) ((triple5 ((triple5 triple1) -> rule2)) -> rule4)) -> rule6) OR ((((triple5 triple1) -> rule2) ((((triple3) -> rule3) triple3) -> rule4)) -> rule6) OR ((((triple5 ((triple5) -> rule1)) -> rule2) ((triple5 triple3) -> rule4)) -> rule6) OR ((((triple5 triple1) -> rule2) ((((triple3) -> rule3) ((triple5 triple1) -> rule2)) -> rule4)) -> rule6) OR ((((triple5 ((triple5) -> rule1)) -> rule2) ((triple5 ((triple5 triple1) -> rule2)) -> rule4)) -> rule6) OR ((((triple5 ((triple5) -> rule1)) -> rule2) ((((triple3) -> rule3) triple3) -> rule4)) -> rule6) OR ((((triple5 ((triple5) -> rule1)) -> rule2) ((((triple3) -> rule3) ((triple5 triple1) -> rule2)) -> rule4)) -> rule6) OR ((triple3 ((triple5 ((triple5 ((triple5) -> rule1)) -> rule2)) -> rule4)) -> rule6) OR ((triple3 ((((triple3) -> rule3) ((triple5 ((triple5) -> rule1)) -> rule2)) -> rule4)) -> rule6) OR ((((triple5 triple1) -> rule2) ((triple5 ((triple5 ((triple5) -> rule1)) -> rule2)) -> rule4)) -> rule6) OR ((((triple5 triple1) -> rule2) ((((triple3) -> rule3) ((triple5 ((triple5) -> rule1)) -> rule2)) -> rule4)) -> rule6) OR ((((triple5 ((triple5) -> rule1)) -> rule2) ((triple5 ((triple5 ((triple5) -> rule1)) -> rule2)) -> rule4)) -> rule6) OR ((((triple5 ((triple5) -> rule1)) -> rule2) ((((triple3) -> rule3) ((triple5 ((triple5) -> rule1)) -> rule2)) -> rule4)) -> rule6))] The cow is red.[(triple5 OR ((triple3) -> rule3))]
The cow is big.
("cow" "is" "big" "+")
triple1
((triple5) -> (rule1 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow is blue.
("cow" "is" "blue" "+")
triple2
((triple5 triple3) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
((triple5 ((triple5 triple1) -> (rule2 % int2))) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
((((triple3) -> (rule3 % int2)) triple3) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
((((triple3) -> (rule3 % int3)) ((triple5 triple1) -> (rule2 % int2))) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
((triple5 ((triple5 ((triple5) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow is big.
("cow" "is" "big" "+")
int3
((((triple3) -> (rule3 % int4)) ((triple5 ((triple5) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow is big.
("cow" "is" "big" "+")
int3
The cow is red.
("cow" "is" "red" "+")
int4
The cow is cold.
("cow" "is" "cold" "+")
triple3
((triple5 triple1) -> (rule2 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
((triple5 ((triple5) -> (rule1 % int2))) -> (rule2 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
triple4
((triple3 triple2) -> (rule6 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
((triple3 ((triple5 triple3) -> (rule4 % int2))) -> (rule6 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
((((triple5 triple1) -> (rule2 % int2)) triple2) -> (rule6 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
((((triple5 triple1) -> (rule2 % int3)) ((triple5 triple3) -> (rule4 % int2))) -> (rule6 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
((triple3 ((triple5 ((triple5 triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
((triple3 ((((triple3) -> (rule3 % int3)) triple3) -> (rule4 % int2))) -> (rule6 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
((((triple5 ((triple5) -> (rule1 % int3))) -> (rule2 % int2)) triple2) -> (rule6 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow is big.
("cow" "is" "big" "+")
int3
((triple3 ((((triple3) -> (rule3 % int4)) ((triple5 triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The cow is red.
("cow" "is" "red" "+")
int4
((((triple5 triple1) -> (rule2 % int3)) ((triple5 ((triple5 triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
((((triple5 triple1) -> (rule2 % int4)) ((((triple3) -> (rule3 % int3)) triple3) -> (rule4 % int2))) -> (rule6 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
The cow is cold.
("cow" "is" "cold" "+")
int4
((((triple5 ((triple5) -> (rule1 % int4))) -> (rule2 % int3)) ((triple5 triple3) -> (rule4 % int2))) -> (rule6 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The cow is big.
("cow" "is" "big" "+")
int4
((((triple5 triple1) -> (rule2 % int4)) ((((triple3) -> (rule3 % int3)) ((triple5 triple1) -> (rule2 % int4))) -> (rule4 % int2))) -> (rule6 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
The cow is cold.
("cow" "is" "cold" "+")
int4
((((triple5 ((triple5) -> (rule1 % int4))) -> (rule2 % int3)) ((triple5 ((triple5 triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The cow is big.
("cow" "is" "big" "+")
int4
((((triple5 ((triple5) -> (rule1 % int5))) -> (rule2 % int4)) ((((triple3) -> (rule3 % int3)) triple3) -> (rule4 % int2))) -> (rule6 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
The cow is cold.
("cow" "is" "cold" "+")
int4
The cow is big.
("cow" "is" "big" "+")
int5
((((triple5 ((triple5) -> (rule1 % int5))) -> (rule2 % int4)) ((((triple3) -> (rule3 % int3)) ((triple5 triple1) -> (rule2 % int4))) -> (rule4 % int2))) -> (rule6 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
The cow is cold.
("cow" "is" "cold" "+")
int4
The cow is big.
("cow" "is" "big" "+")
int5
((triple3 ((triple5 ((triple5 ((triple5) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The cow is big.
("cow" "is" "big" "+")
int4
((triple3 ((((triple3) -> (rule3 % int5)) ((triple5 ((triple5) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The cow is big.
("cow" "is" "big" "+")
int4
The cow is red.
("cow" "is" "red" "+")
int5
((((triple5 triple1) -> (rule2 % int4)) ((triple5 ((triple5 ((triple5) -> (rule1 % int3))) -> (rule2 % int4))) -> (rule4 % int2))) -> (rule6 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is big.
("cow" "is" "big" "+")
int3
The cow is cold.
("cow" "is" "cold" "+")
int4
((((triple5 triple1) -> (rule2 % int5)) ((((triple3) -> (rule3 % int4)) ((triple5 ((triple5) -> (rule1 % int3))) -> (rule2 % int5))) -> (rule4 % int2))) -> (rule6 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is big.
("cow" "is" "big" "+")
int3
The cow is red.
("cow" "is" "red" "+")
int4
The cow is cold.
("cow" "is" "cold" "+")
int5
((((triple5 ((triple5) -> (rule1 % int4))) -> (rule2 % int3)) ((triple5 ((triple5 ((triple5) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The cow is big.
("cow" "is" "big" "+")
int4
((((triple5 ((triple5) -> (rule1 % int5))) -> (rule2 % int4)) ((((triple3) -> (rule3 % int3)) ((triple5 ((triple5) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule4 % int2))) -> (rule6 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
The cow is cold.
("cow" "is" "cold" "+")
int4
The cow is big.
("cow" "is" "big" "+")
int5
The cow is red.
("cow" "is" "red" "+")
triple5
((triple3) -> (rule3 % int1))
The cow is red.
("cow" "is" "red" "+")
int1