The cat is blue. The cat is cold. The cat is kind. Blue, red people are nice. Cold, blue people are nice. If the cat is cold and the cat is kind then the cat is blue. All nice, kind people are red. If the cat is nice and the cat is kind then the cat is red. Blue people are kind.
The cat is blue.
("cat" "is" "blue" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is kind.
("cat" "is" "kind" "+")
Blue, red people are nice.
((("someone" "is" "blue" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
Cold, blue people are nice.
((("someone" "is" "cold" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
If the cat is cold and the cat is kind then the cat is blue.
((("cat" "is" "cold" "+") ("cat" "is" "kind" "+")) -> ("cat" "is" "blue" "+"))
All nice, kind people are red.
((("someone" "is" "nice" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
If the cat is nice and the cat is kind then the cat is red.
((("cat" "is" "nice" "+") ("cat" "is" "kind" "+")) -> ("cat" "is" "red" "+"))
Blue people are kind.
((("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
The cat is kind.
True
1
proof
[(triple3 OR ((triple1) -> rule6))]
("cat" "is" "kind" "+")
triple3
((triple1) -> (rule6 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is not blue.
False
1
inv-proof
[(triple1 OR ((triple2 triple3) -> rule3))]
("cat" "is" "blue" "-")
triple1
((triple2 triple3) -> (rule3 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat is nice.
True
3
proof
[(((triple2 triple1) -> rule2) OR ((triple2 ((triple2 triple3) -> rule3)) -> rule2))]
("cat" "is" "nice" "+")
((triple2 triple1) -> (rule2 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
((triple2 ((triple2 triple3) -> (rule3 % int2))) -> (rule2 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The cat is not nice.
False
3
inv-proof
[(((triple2 triple1) -> rule2) OR ((triple2 ((triple2 triple3) -> rule3)) -> rule2))]
("cat" "is" "nice" "-")
((triple2 triple1) -> (rule2 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
((triple2 ((triple2 triple3) -> (rule3 % int2))) -> (rule2 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The cat is red.
True
5
proof
[(((((triple2 triple1) -> rule2) triple3) -> rule4) OR ((((triple2 triple1) -> rule2) triple3) -> rule5) OR ((((triple2 triple1) -> rule2) ((triple1) -> rule6)) -> rule4) OR ((((triple2 triple1) -> rule2) ((triple1) -> rule6)) -> rule5) OR ((((triple2 ((triple2 triple3) -> rule3)) -> rule2) triple3) -> rule4) OR ((((triple2 ((triple2 triple3) -> rule3)) -> rule2) triple3) -> rule5) OR ((((triple2 ((triple2 triple3) -> rule3)) -> rule2) ((triple1) -> rule6)) -> rule4) OR ((((triple2 ((triple2 triple3) -> rule3)) -> rule2) ((triple1) -> rule6)) -> rule5))]
("cat" "is" "red" "+")
((((triple2 triple1) -> (rule2 % int2)) triple3) -> (rule4 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
((((triple2 triple1) -> (rule2 % int2)) triple3) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
((((triple2 triple1) -> (rule2 % int3)) ((triple1) -> (rule6 % int2))) -> (rule4 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
int3
((((triple2 triple1) -> (rule2 % int3)) ((triple1) -> (rule6 % int2))) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
int3
((((triple2 ((triple2 triple3) -> (rule3 % int3))) -> (rule2 % int2)) triple3) -> (rule4 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat is blue.
("cat" "is" "blue" "+")
int3
((((triple2 ((triple2 triple3) -> (rule3 % int3))) -> (rule2 % int2)) triple3) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat is blue.
("cat" "is" "blue" "+")
int3
((((triple2 ((triple2 triple3) -> (rule3 % int4))) -> (rule2 % int3)) ((triple1) -> (rule6 % int2))) -> (rule4 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
int3
The cat is blue.
("cat" "is" "blue" "+")
int4
((((triple2 ((triple2 triple3) -> (rule3 % int4))) -> (rule2 % int3)) ((triple1) -> (rule6 % int2))) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
int3
The cat is blue.
("cat" "is" "blue" "+")
int4
The cat is not red.
False
5
inv-proof
[(((((triple2 triple1) -> rule2) triple3) -> rule4) OR ((((triple2 triple1) -> rule2) triple3) -> rule5) OR ((((triple2 triple1) -> rule2) ((triple1) -> rule6)) -> rule4) OR ((((triple2 triple1) -> rule2) ((triple1) -> rule6)) -> rule5) OR ((((triple2 ((triple2 triple3) -> rule3)) -> rule2) triple3) -> rule4) OR ((((triple2 ((triple2 triple3) -> rule3)) -> rule2) triple3) -> rule5) OR ((((triple2 ((triple2 triple3) -> rule3)) -> rule2) ((triple1) -> rule6)) -> rule4) OR ((((triple2 ((triple2 triple3) -> rule3)) -> rule2) ((triple1) -> rule6)) -> rule5))]
("cat" "is" "red" "-")
((((triple2 triple1) -> (rule2 % int2)) triple3) -> (rule4 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
((((triple2 triple1) -> (rule2 % int2)) triple3) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
((((triple2 triple1) -> (rule2 % int3)) ((triple1) -> (rule6 % int2))) -> (rule4 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
int3
((((triple2 triple1) -> (rule2 % int3)) ((triple1) -> (rule6 % int2))) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
int3
((((triple2 ((triple2 triple3) -> (rule3 % int3))) -> (rule2 % int2)) triple3) -> (rule4 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat is blue.
("cat" "is" "blue" "+")
int3
((((triple2 ((triple2 triple3) -> (rule3 % int3))) -> (rule2 % int2)) triple3) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat is blue.
("cat" "is" "blue" "+")
int3
((((triple2 ((triple2 triple3) -> (rule3 % int4))) -> (rule2 % int3)) ((triple1) -> (rule6 % int2))) -> (rule4 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
int3
The cat is blue.
("cat" "is" "blue" "+")
int4
((((triple2 ((triple2 triple3) -> (rule3 % int4))) -> (rule2 % int3)) ((triple1) -> (rule6 % int2))) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
int3
The cat is blue.
("cat" "is" "blue" "+")
int4
The cat does not see the cat.
Unknown
inv-random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "-")
The cat visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
@0: The cat is blue.[(triple1 OR ((triple2 triple3) -> rule3))] The cat is cold.[(triple2)] The cat is kind.[(triple3 OR ((triple1) -> rule6))] @1: The cat is nice.[(((triple2 triple1) -> rule2) OR ((triple2 ((triple2 triple3) -> rule3)) -> rule2))] @2: The cat is red.[(((((triple2 triple1) -> rule2) triple3) -> rule4) OR ((((triple2 triple1) -> rule2) triple3) -> rule5) OR ((((triple2 triple1) -> rule2) ((triple1) -> rule6)) -> rule4) OR ((((triple2 triple1) -> rule2) ((triple1) -> rule6)) -> rule5) OR ((((triple2 ((triple2 triple3) -> rule3)) -> rule2) triple3) -> rule4) OR ((((triple2 ((triple2 triple3) -> rule3)) -> rule2) triple3) -> rule5) OR ((((triple2 ((triple2 triple3) -> rule3)) -> rule2) ((triple1) -> rule6)) -> rule4) OR ((((triple2 ((triple2 triple3) -> rule3)) -> rule2) ((triple1) -> rule6)) -> rule5))]
The cat is blue.
("cat" "is" "blue" "+")
triple1
((triple2 triple3) -> (rule3 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
triple2
The cat is kind.
("cat" "is" "kind" "+")
triple3
((triple1) -> (rule6 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
((triple2 triple1) -> (rule2 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
((triple2 ((triple2 triple3) -> (rule3 % int2))) -> (rule2 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The cat is red.
("cat" "is" "red" "+")
((((triple2 triple1) -> (rule2 % int2)) triple3) -> (rule4 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
((((triple2 triple1) -> (rule2 % int2)) triple3) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
((((triple2 triple1) -> (rule2 % int3)) ((triple1) -> (rule6 % int2))) -> (rule4 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
int3
((((triple2 triple1) -> (rule2 % int3)) ((triple1) -> (rule6 % int2))) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
int3
((((triple2 ((triple2 triple3) -> (rule3 % int3))) -> (rule2 % int2)) triple3) -> (rule4 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat is blue.
("cat" "is" "blue" "+")
int3
((((triple2 ((triple2 triple3) -> (rule3 % int3))) -> (rule2 % int2)) triple3) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat is blue.
("cat" "is" "blue" "+")
int3
((((triple2 ((triple2 triple3) -> (rule3 % int4))) -> (rule2 % int3)) ((triple1) -> (rule6 % int2))) -> (rule4 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
int3
The cat is blue.
("cat" "is" "blue" "+")
int4
((((triple2 ((triple2 triple3) -> (rule3 % int4))) -> (rule2 % int3)) ((triple1) -> (rule6 % int2))) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
int3
The cat is blue.
("cat" "is" "blue" "+")
int4