The bear chases the cat. The bear is not rough. The bear is young. The bear likes the cat. The bear does not need the cat. The cat chases the bear. The cat is blue. The cat is red. The cat is not rough. The cat is young. If something chases the cat then the cat is round. If something likes the cat and the cat chases the bear then the cat is round. If something is round and it chases the bear then it chases the cat. If the bear chases the cat and the bear is rough then the bear likes the cat. If something is rough and young then it is blue. If something chases the cat and the cat is round then it likes the cat. If something is young then it does not need the bear. If something is round and it does not need the bear then it does not need the cat.
The bear chases the cat.
("bear" "chases" "cat" "+")
The bear is not rough.
("bear" "is" "rough" "-")
The bear is young.
("bear" "is" "young" "+")
The bear likes the cat.
("bear" "likes" "cat" "+")
The bear does not need the cat.
("bear" "needs" "cat" "-")
The cat chases the bear.
("cat" "chases" "bear" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is red.
("cat" "is" "red" "+")
The cat is not rough.
("cat" "is" "rough" "-")
The cat is young.
("cat" "is" "young" "+")
If something chases the cat then the cat is round.
((("something" "chases" "cat" "+")) -> ("cat" "is" "round" "+"))
If something likes the cat and the cat chases the bear then the cat is round.
((("something" "likes" "cat" "+") ("cat" "chases" "bear" "+")) -> ("cat" "is" "round" "+"))
If something is round and it chases the bear then it chases the cat.
((("something" "is" "round" "+") ("something" "chases" "bear" "+")) -> ("something" "chases" "cat" "+"))
If the bear chases the cat and the bear is rough then the bear likes the cat.
((("bear" "chases" "cat" "+") ("bear" "is" "rough" "+")) -> ("bear" "likes" "cat" "+"))
If something is rough and young then it is blue.
((("something" "is" "rough" "+") ("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
If something chases the cat and the cat is round then it likes the cat.
((("something" "chases" "cat" "+") ("cat" "is" "round" "+")) -> ("something" "likes" "cat" "+"))
If something is young then it does not need the bear.
((("something" "is" "young" "+")) -> ("something" "needs" "bear" "-"))
If something is round and it does not need the bear then it does not need the cat.
((("something" "is" "round" "+") ("something" "needs" "bear" "~")) -> ("something" "needs" "cat" "-"))
The cat chases the bear.
True
1
proof
[(triple6)]
("cat" "chases" "bear" "+")
triple6
The bear is not young.
False
1
inv-proof
[(triple3)]
("bear" "is" "young" "-")
triple3
The cat is round.
True
2
proof
[(((triple1) -> rule1) OR ((triple4 triple6) -> rule2))]
("cat" "is" "round" "+")
((triple1) -> (rule1 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
((triple4 triple6) -> (rule2 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The bear needs the bear.
False
2
inv-proof
[(((triple3) -> rule7))]
("bear" "needs" "bear" "+")
((triple3) -> (rule7 % int1))
The bear does not need the bear.
("bear" "needs" "bear" "-")
int1
The cat chases the cat.
True
4
proof
[(((((triple1) -> rule1) triple6) -> rule3) OR ((((triple4 triple6) -> rule2) triple6) -> rule3))]
("cat" "chases" "cat" "+")
((((triple1) -> (rule1 % int2)) triple6) -> (rule3 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
((((triple4 triple6) -> (rule2 % int2)) triple6) -> (rule3 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat needs the cat.
False
5
inv-proof
[(((((triple1) -> rule1) ((triple10) -> rule7)) -> rule8) OR ((((triple4 triple6) -> rule2) ((triple10) -> rule7)) -> rule8))]
("cat" "needs" "cat" "+")
((((triple1) -> (rule1 % int3)) ((triple10) -> (rule7 % int2))) -> (rule8 % int1))
The cat does not need the cat.
("cat" "needs" "cat" "-")
int1
The cat does not need the bear.
("cat" "needs" "bear" "-")
int2
The cat is round.
("cat" "is" "round" "+")
int3
((((triple4 triple6) -> (rule2 % int3)) ((triple10) -> (rule7 % int2))) -> (rule8 % int1))
The cat does not need the cat.
("cat" "needs" "cat" "-")
int1
The cat does not need the bear.
("cat" "needs" "bear" "-")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The cat likes the cat.
True
7
proof
[(((((((triple1) -> rule1) triple6) -> rule3) ((triple1) -> rule1)) -> rule6) OR ((((((triple1) -> rule1) triple6) -> rule3) ((triple4 triple6) -> rule2)) -> rule6) OR ((((((triple4 triple6) -> rule2) triple6) -> rule3) ((triple1) -> rule1)) -> rule6) OR ((((((triple4 triple6) -> rule2) triple6) -> rule3) ((triple4 triple6) -> rule2)) -> rule6))]
("cat" "likes" "cat" "+")
((((((triple1) -> (rule1 % int3)) triple6) -> (rule3 % int2)) ((triple1) -> (rule1 % int3))) -> (rule6 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
((((((triple1) -> (rule1 % int3)) triple6) -> (rule3 % int2)) ((triple4 triple6) -> (rule2 % int3))) -> (rule6 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
((((((triple4 triple6) -> (rule2 % int3)) triple6) -> (rule3 % int2)) ((triple1) -> (rule1 % int3))) -> (rule6 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
((((((triple4 triple6) -> (rule2 % int3)) triple6) -> (rule3 % int2)) ((triple4 triple6) -> (rule2 % int3))) -> (rule6 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The cat does not like the cat.
False
7
inv-proof
[(((((((triple1) -> rule1) triple6) -> rule3) ((triple1) -> rule1)) -> rule6) OR ((((((triple1) -> rule1) triple6) -> rule3) ((triple4 triple6) -> rule2)) -> rule6) OR ((((((triple4 triple6) -> rule2) triple6) -> rule3) ((triple1) -> rule1)) -> rule6) OR ((((((triple4 triple6) -> rule2) triple6) -> rule3) ((triple4 triple6) -> rule2)) -> rule6))]
("cat" "likes" "cat" "-")
((((((triple1) -> (rule1 % int3)) triple6) -> (rule3 % int2)) ((triple1) -> (rule1 % int3))) -> (rule6 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
((((((triple1) -> (rule1 % int3)) triple6) -> (rule3 % int2)) ((triple4 triple6) -> (rule2 % int3))) -> (rule6 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
((((((triple4 triple6) -> (rule2 % int3)) triple6) -> (rule3 % int2)) ((triple1) -> (rule1 % int3))) -> (rule6 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
((((((triple4 triple6) -> (rule2 % int3)) triple6) -> (rule3 % int2)) ((triple4 triple6) -> (rule2 % int3))) -> (rule6 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The bear is not blue.
Unknown
inv-rconc
[@1: The bear is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "is" "blue" "-")
The cat likes the bear.
Unknown
random
[@0: The cat likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "bear" "+")
The bear does not chase the bear.
Unknown
inv-random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "-")
The bear likes the bear.
Unknown
random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "+")
The bear is not round.
Unknown
inv-random
[@0: The bear is round.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "round" "-")
The bear is red.
Unknown
random
[@0: The bear is red.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "red" "+")
@0: The bear chases the cat.[(triple1)] The bear does not need the cat.[(triple5)] The bear is not rough.[(triple2)] The bear is young.[(triple3)] The bear likes the cat.[(triple4 OR ((triple1 ((triple1) -> rule1)) -> rule6))] The cat chases the bear.[(triple6)] The cat is blue.[(triple7)] The cat is not rough.[(triple9)] The cat is red.[(triple8)] The cat is young.[(triple10)] @1: The bear does not need the bear.[(((triple3) -> rule7))] The cat does not need the bear.[(((triple10) -> rule7))] The cat is round.[(((triple1) -> rule1) OR ((triple4 triple6) -> rule2))] @2: The cat chases the cat.[(((((triple1) -> rule1) triple6) -> rule3) OR ((((triple4 triple6) -> rule2) triple6) -> rule3))] The cat does not need the cat.[(((((triple1) -> rule1) ((triple10) -> rule7)) -> rule8) OR ((((triple4 triple6) -> rule2) ((triple10) -> rule7)) -> rule8))] @3: The cat likes the cat.[(((((((triple1) -> rule1) triple6) -> rule3) ((triple1) -> rule1)) -> rule6) OR ((((((triple1) -> rule1) triple6) -> rule3) ((triple4 triple6) -> rule2)) -> rule6) OR ((((((triple4 triple6) -> rule2) triple6) -> rule3) ((triple1) -> rule1)) -> rule6) OR ((((((triple4 triple6) -> rule2) triple6) -> rule3) ((triple4 triple6) -> rule2)) -> rule6))]
The bear chases the cat.
("bear" "chases" "cat" "+")
triple1
The bear does not need the cat.
("bear" "needs" "cat" "-")
triple5
The bear is not rough.
("bear" "is" "rough" "-")
triple2
The bear is young.
("bear" "is" "young" "+")
triple3
The bear likes the cat.
("bear" "likes" "cat" "+")
triple4
((triple1 ((triple1) -> (rule1 % int2))) -> (rule6 % int1))
The bear likes the cat.
("bear" "likes" "cat" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat chases the bear.
("cat" "chases" "bear" "+")
triple6
The cat is blue.
("cat" "is" "blue" "+")
triple7
The cat is not rough.
("cat" "is" "rough" "-")
triple9
The cat is red.
("cat" "is" "red" "+")
triple8
The cat is young.
("cat" "is" "young" "+")
triple10
The bear does not need the bear.
("bear" "needs" "bear" "-")
((triple3) -> (rule7 % int1))
The bear does not need the bear.
("bear" "needs" "bear" "-")
int1
The cat does not need the bear.
("cat" "needs" "bear" "-")
((triple10) -> (rule7 % int1))
The cat does not need the bear.
("cat" "needs" "bear" "-")
int1
The cat is round.
("cat" "is" "round" "+")
((triple1) -> (rule1 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
((triple4 triple6) -> (rule2 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
((((triple1) -> (rule1 % int2)) triple6) -> (rule3 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
((((triple4 triple6) -> (rule2 % int2)) triple6) -> (rule3 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat does not need the cat.
("cat" "needs" "cat" "-")
((((triple1) -> (rule1 % int3)) ((triple10) -> (rule7 % int2))) -> (rule8 % int1))
The cat does not need the cat.
("cat" "needs" "cat" "-")
int1
The cat does not need the bear.
("cat" "needs" "bear" "-")
int2
The cat is round.
("cat" "is" "round" "+")
int3
((((triple4 triple6) -> (rule2 % int3)) ((triple10) -> (rule7 % int2))) -> (rule8 % int1))
The cat does not need the cat.
("cat" "needs" "cat" "-")
int1
The cat does not need the bear.
("cat" "needs" "bear" "-")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The cat likes the cat.
("cat" "likes" "cat" "+")
((((((triple1) -> (rule1 % int3)) triple6) -> (rule3 % int2)) ((triple1) -> (rule1 % int3))) -> (rule6 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
((((((triple1) -> (rule1 % int3)) triple6) -> (rule3 % int2)) ((triple4 triple6) -> (rule2 % int3))) -> (rule6 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
((((((triple4 triple6) -> (rule2 % int3)) triple6) -> (rule3 % int2)) ((triple1) -> (rule1 % int3))) -> (rule6 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
((((((triple4 triple6) -> (rule2 % int3)) triple6) -> (rule3 % int2)) ((triple4 triple6) -> (rule2 % int3))) -> (rule6 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3