The cat is blue. The cat is cold. The cat is kind. If the cat is kind and the cat is red then the cat is green. Cold, blue things are red. All red things are green. All green things are kind. If the cat is cold and the cat is green then the cat is kind. All cold things are blue.
The cat is blue.
("cat" "is" "blue" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is kind.
("cat" "is" "kind" "+")
If the cat is kind and the cat is red then the cat is green.
((("cat" "is" "kind" "+") ("cat" "is" "red" "+")) -> ("cat" "is" "green" "+"))
Cold, blue things are red.
((("something" "is" "cold" "+") ("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
All red things are green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
All green things are kind.
((("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
If the cat is cold and the cat is green then the cat is kind.
((("cat" "is" "cold" "+") ("cat" "is" "green" "+")) -> ("cat" "is" "kind" "+"))
All cold things are blue.
((("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
The cat is blue.
True
1
proof
[(triple1 OR ((triple2) -> rule6))]
("cat" "is" "blue" "+")
triple1
((triple2) -> (rule6 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat is not kind.
False
1
inv-proof
[(triple3 OR ((((((triple2 triple1) -> rule2)) -> rule3)) -> rule4) OR ((triple2 ((((triple2 triple1) -> rule2)) -> rule3)) -> rule5) OR ((((((triple2 ((triple2) -> rule6)) -> rule2)) -> rule3)) -> rule4) OR ((triple2 ((((triple2 ((triple2) -> rule6)) -> rule2)) -> rule3)) -> rule5))]
("cat" "is" "kind" "-")
triple3
((((((triple2 triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
((triple2 ((((triple2 triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
((((((triple2 ((triple2) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
The cat is blue.
("cat" "is" "blue" "+")
int4
((triple2 ((((triple2 ((triple2) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
The cat is blue.
("cat" "is" "blue" "+")
int4
The cat is red.
True
3
proof
[(((triple2 triple1) -> rule2) OR ((triple2 ((triple2) -> rule6)) -> rule2))]
("cat" "is" "red" "+")
((triple2 triple1) -> (rule2 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
((triple2 ((triple2) -> (rule6 % int2))) -> (rule2 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The cat is not red.
False
3
inv-proof
[(((triple2 triple1) -> rule2) OR ((triple2 ((triple2) -> rule6)) -> rule2))]
("cat" "is" "red" "-")
((triple2 triple1) -> (rule2 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
((triple2 ((triple2) -> (rule6 % int2))) -> (rule2 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The cat is green.
True
4
proof
[(((((triple2 triple1) -> rule2)) -> rule3) OR ((triple3 ((triple2 triple1) -> rule2)) -> rule1) OR ((((triple2 ((triple2) -> rule6)) -> rule2)) -> rule3) OR ((triple3 ((triple2 ((triple2) -> rule6)) -> rule2)) -> rule1))]
("cat" "is" "green" "+")
((((triple2 triple1) -> (rule2 % int2))) -> (rule3 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
((triple3 ((triple2 triple1) -> (rule2 % int2))) -> (rule1 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
((((triple2 ((triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat is blue.
("cat" "is" "blue" "+")
int3
((triple3 ((triple2 ((triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat is blue.
("cat" "is" "blue" "+")
int3
The cat is not green.
False
4
inv-proof
[(((((triple2 triple1) -> rule2)) -> rule3) OR ((triple3 ((triple2 triple1) -> rule2)) -> rule1) OR ((((triple2 ((triple2) -> rule6)) -> rule2)) -> rule3) OR ((triple3 ((triple2 ((triple2) -> rule6)) -> rule2)) -> rule1))]
("cat" "is" "green" "-")
((((triple2 triple1) -> (rule2 % int2))) -> (rule3 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
((triple3 ((triple2 triple1) -> (rule2 % int2))) -> (rule1 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
((((triple2 ((triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat is blue.
("cat" "is" "blue" "+")
int3
((triple3 ((triple2 ((triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat is blue.
("cat" "is" "blue" "+")
int3
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) -> rule6))] The cat is cold.[(triple2)] The cat is kind.[(triple3 OR ((((((triple2 triple1) -> rule2)) -> rule3)) -> rule4) OR ((triple2 ((((triple2 triple1) -> rule2)) -> rule3)) -> rule5) OR ((((((triple2 ((triple2) -> rule6)) -> rule2)) -> rule3)) -> rule4) OR ((triple2 ((((triple2 ((triple2) -> rule6)) -> rule2)) -> rule3)) -> rule5))] @1: The cat is red.[(((triple2 triple1) -> rule2) OR ((triple2 ((triple2) -> rule6)) -> rule2))] @2: The cat is green.[(((((triple2 triple1) -> rule2)) -> rule3) OR ((triple3 ((triple2 triple1) -> rule2)) -> rule1) OR ((((triple2 ((triple2) -> rule6)) -> rule2)) -> rule3) OR ((triple3 ((triple2 ((triple2) -> rule6)) -> rule2)) -> rule1))]
The cat is blue.
("cat" "is" "blue" "+")
triple1
((triple2) -> (rule6 % 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
((((((triple2 triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
((triple2 ((((triple2 triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
((((((triple2 ((triple2) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
The cat is blue.
("cat" "is" "blue" "+")
int4
((triple2 ((((triple2 ((triple2) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
The cat is blue.
("cat" "is" "blue" "+")
int4
The cat is red.
("cat" "is" "red" "+")
((triple2 triple1) -> (rule2 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
((triple2 ((triple2) -> (rule6 % int2))) -> (rule2 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The cat is green.
("cat" "is" "green" "+")
((((triple2 triple1) -> (rule2 % int2))) -> (rule3 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
((triple3 ((triple2 triple1) -> (rule2 % int2))) -> (rule1 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
((((triple2 ((triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat is blue.
("cat" "is" "blue" "+")
int3
((triple3 ((triple2 ((triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat is blue.
("cat" "is" "blue" "+")
int3