The bear eats the cat. The bear is red. The bear is rough. The bear needs the cat. The cat eats the bear. The cat is cold. The cat is red. The cat is rough. The cat needs the bear. The cat visits the bear. If something visits the bear then it eats the cat. If the cat is round then the cat needs the bear. If something eats the bear then it is round. If something eats the bear then the bear visits the cat. All round, red things are green. If something is red then it eats the bear.
The bear eats the cat.
("bear" "eats" "cat" "+")
The bear is red.
("bear" "is" "red" "+")
The bear is rough.
("bear" "is" "rough" "+")
The bear needs the cat.
("bear" "needs" "cat" "+")
The cat eats the bear.
("cat" "eats" "bear" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is red.
("cat" "is" "red" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat needs the bear.
("cat" "needs" "bear" "+")
The cat visits the bear.
("cat" "visits" "bear" "+")
If something visits the bear then it eats the cat.
((("something" "visits" "bear" "+")) -> ("something" "eats" "cat" "+"))
If the cat is round then the cat needs the bear.
((("cat" "is" "round" "+")) -> ("cat" "needs" "bear" "+"))
If something eats the bear then it is round.
((("something" "eats" "bear" "+")) -> ("something" "is" "round" "+"))
If something eats the bear then the bear visits the cat.
((("something" "eats" "bear" "+")) -> ("bear" "visits" "cat" "+"))
All round, red things are green.
((("something" "is" "round" "+") ("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
If something is red then it eats the bear.
((("something" "is" "red" "+")) -> ("something" "eats" "bear" "+"))
The bear is red.
True
1
proof
[(triple2)]
("bear" "is" "red" "+")
triple2
The cat does not eat the bear.
False
1
inv-proof
[(triple5 OR ((triple7) -> rule6))]
("cat" "eats" "bear" "-")
triple5
((triple7) -> (rule6 % int1))
The cat eats the bear.
("cat" "eats" "bear" "+")
int1
The bear visits the cat.
True
2
proof
[(((triple5) -> rule4) OR ((((triple2) -> rule6)) -> rule4) OR ((((triple7) -> rule6)) -> rule4))]
("bear" "visits" "cat" "+")
((triple5) -> (rule4 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1
The bear eats the bear.
("bear" "eats" "bear" "+")
int2
((((triple7) -> (rule6 % int2))) -> (rule4 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1
The cat eats the bear.
("cat" "eats" "bear" "+")
int2
The bear does not eat the bear.
False
2
inv-proof
[(((triple2) -> rule6))]
("bear" "eats" "bear" "-")
((triple2) -> (rule6 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The cat is green.
True
4
proof
[(((((triple5) -> rule3) triple7) -> rule5) OR ((((((triple7) -> rule6)) -> rule3) triple7) -> rule5))]
("cat" "is" "green" "+")
((((triple5) -> (rule3 % int2)) triple7) -> (rule5 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
((((((triple7) -> (rule6 % int3))) -> (rule3 % int2)) triple7) -> (rule5 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat eats the bear.
("cat" "eats" "bear" "+")
int3
The bear is not round.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule3))]
("bear" "is" "round" "-")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The bear eats the bear.
("bear" "eats" "bear" "+")
int2
The bear is green.
True
5
proof
[(((((((triple2) -> rule6)) -> rule3) triple2) -> rule5))]
("bear" "is" "green" "+")
((((((triple2) -> (rule6 % int3))) -> (rule3 % int2)) triple2) -> (rule5 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The bear eats the bear.
("bear" "eats" "bear" "+")
int3
The bear is not green.
False
5
inv-proof
[(((((((triple2) -> rule6)) -> rule3) triple2) -> rule5))]
("bear" "is" "green" "-")
((((((triple2) -> (rule6 % int3))) -> (rule3 % int2)) triple2) -> (rule5 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The bear eats the bear.
("bear" "eats" "bear" "+")
int3
The bear is not cold.
Unknown
inv-random
[@0: The bear is cold.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "cold" "-")
The bear needs the bear.
Unknown
random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "+")
The cat does not need the cat.
Unknown
inv-random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "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 bear eats the cat.[(triple1)] The bear is red.[(triple2)] The bear is rough.[(triple3)] The bear needs the cat.[(triple4)] The cat eats the bear.[(triple5 OR ((triple7) -> rule6))] The cat is cold.[(triple6)] The cat is red.[(triple7)] The cat is rough.[(triple8)] The cat needs the bear.[(triple9 OR ((((triple5) -> rule3)) -> rule2) OR ((((((triple7) -> rule6)) -> rule3)) -> rule2))] The cat visits the bear.[(triple10)] @1: The bear eats the bear.[(((triple2) -> rule6))] The bear visits the cat.[(((triple5) -> rule4) OR ((((triple2) -> rule6)) -> rule4) OR ((((triple7) -> rule6)) -> rule4))] The cat eats the cat.[(((triple10) -> rule1))] The cat is round.[(((triple5) -> rule3) OR ((((triple7) -> rule6)) -> rule3))] @2: The bear is round.[(((((triple2) -> rule6)) -> rule3))] The cat is green.[(((((triple5) -> rule3) triple7) -> rule5) OR ((((((triple7) -> rule6)) -> rule3) triple7) -> rule5))] @3: The bear is green.[(((((((triple2) -> rule6)) -> rule3) triple2) -> rule5))]
The bear eats the cat.
("bear" "eats" "cat" "+")
triple1
The bear is red.
("bear" "is" "red" "+")
triple2
The bear is rough.
("bear" "is" "rough" "+")
triple3
The bear needs the cat.
("bear" "needs" "cat" "+")
triple4
The cat eats the bear.
("cat" "eats" "bear" "+")
triple5
((triple7) -> (rule6 % int1))
The cat eats the bear.
("cat" "eats" "bear" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
triple6
The cat is red.
("cat" "is" "red" "+")
triple7
The cat is rough.
("cat" "is" "rough" "+")
triple8
The cat needs the bear.
("cat" "needs" "bear" "+")
triple9
((((triple5) -> (rule3 % int2))) -> (rule2 % int1))
The cat needs the bear.
("cat" "needs" "bear" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
((((((triple7) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The cat needs the bear.
("cat" "needs" "bear" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat eats the bear.
("cat" "eats" "bear" "+")
int3
The cat visits the bear.
("cat" "visits" "bear" "+")
triple10
The bear eats the bear.
("bear" "eats" "bear" "+")
((triple2) -> (rule6 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The bear visits the cat.
("bear" "visits" "cat" "+")
((triple5) -> (rule4 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1
The bear eats the bear.
("bear" "eats" "bear" "+")
int2
((((triple7) -> (rule6 % int2))) -> (rule4 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1
The cat eats the bear.
("cat" "eats" "bear" "+")
int2
The cat eats the cat.
("cat" "eats" "cat" "+")
((triple10) -> (rule1 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat is round.
("cat" "is" "round" "+")
((triple5) -> (rule3 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
((((triple7) -> (rule6 % int2))) -> (rule3 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat eats the bear.
("cat" "eats" "bear" "+")
int2
The bear is round.
("bear" "is" "round" "+")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The bear eats the bear.
("bear" "eats" "bear" "+")
int2
The cat is green.
("cat" "is" "green" "+")
((((triple5) -> (rule3 % int2)) triple7) -> (rule5 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
((((((triple7) -> (rule6 % int3))) -> (rule3 % int2)) triple7) -> (rule5 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat eats the bear.
("cat" "eats" "bear" "+")
int3
The bear is green.
("bear" "is" "green" "+")
((((((triple2) -> (rule6 % int3))) -> (rule3 % int2)) triple2) -> (rule5 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The bear eats the bear.
("bear" "eats" "bear" "+")
int3