The bear is blue. The bear is young. The bear likes the cat. The bear needs the rabbit. The bear visits the rabbit. The bear visits the squirrel. The cat is blue. The cat is red. The cat needs the bear. The rabbit likes the cat. The rabbit likes the squirrel. The rabbit visits the bear. The squirrel is blue. The squirrel is young. The squirrel visits the rabbit. If something is young and it needs the rabbit then it visits the cat. If something is young and it likes the cat then the cat is round. Red things are round. If something needs the cat and it needs the rabbit then the cat is cold. If something is round then it visits the rabbit. If something visits the rabbit then the rabbit needs the cat.
The bear is blue.
("bear" "is" "blue" "+")
The bear is young.
("bear" "is" "young" "+")
The bear likes the cat.
("bear" "likes" "cat" "+")
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is red.
("cat" "is" "red" "+")
The cat needs the bear.
("cat" "needs" "bear" "+")
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
If something is young and it needs the rabbit then it visits the cat.
((("something" "is" "young" "+") ("something" "needs" "rabbit" "+")) -> ("something" "visits" "cat" "+"))
If something is young and it likes the cat then the cat is round.
((("something" "is" "young" "+") ("something" "likes" "cat" "+")) -> ("cat" "is" "round" "+"))
Red things are round.
((("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
If something needs the cat and it needs the rabbit then the cat is cold.
((("something" "needs" "cat" "+") ("something" "needs" "rabbit" "+")) -> ("cat" "is" "cold" "+"))
If something is round then it visits the rabbit.
((("something" "is" "round" "+")) -> ("something" "visits" "rabbit" "+"))
If something visits the rabbit then the rabbit needs the cat.
((("something" "visits" "rabbit" "+")) -> ("rabbit" "needs" "cat" "+"))
The bear likes the cat.
True
1
proof
[(triple3)]
("bear" "likes" "cat" "+")
triple3
The bear does not like the cat.
False
1
inv-proof
[(triple3)]
("bear" "likes" "cat" "-")
triple3
The cat is round.
True
2
proof
[(((triple8) -> rule3) OR ((triple2 triple3) -> rule2))]
("cat" "is" "round" "+")
((triple8) -> (rule3 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
((triple2 triple3) -> (rule2 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The rabbit does not need the cat.
False
2
inv-proof
[(((triple15) -> rule6) OR ((triple5) -> rule6) OR ((((((triple8) -> rule3)) -> rule5)) -> rule6) OR ((((((triple2 triple3) -> rule2)) -> rule5)) -> rule6))]
("rabbit" "needs" "cat" "-")
((triple15) -> (rule6 % int1))
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int1
((triple5) -> (rule6 % int1))
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int1
((((((triple8) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
((((((triple2 triple3) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The cat visits the rabbit.
True
3
proof
[(((((triple8) -> rule3)) -> rule5) OR ((((triple2 triple3) -> rule2)) -> rule5))]
("cat" "visits" "rabbit" "+")
((((triple8) -> (rule3 % int2))) -> (rule5 % int1))
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
((((triple2 triple3) -> (rule2 % int2))) -> (rule5 % int1))
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat does not visit the rabbit.
False
3
inv-proof
[(((((triple8) -> rule3)) -> rule5) OR ((((triple2 triple3) -> rule2)) -> rule5))]
("cat" "visits" "rabbit" "-")
((((triple8) -> (rule3 % int2))) -> (rule5 % int1))
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
((((triple2 triple3) -> (rule2 % int2))) -> (rule5 % int1))
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat does not visit the cat.
Unknown
inv-rconc
[@1: The cat visits the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "visits" "cat" "-")
The squirrel is round.
Unknown
rconc
[@1: The squirrel is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "is" "round" "+")
The rabbit does not visit the cat.
Unknown
inv-rconc
[@1: The rabbit visits the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "visits" "cat" "-")
The squirrel likes the squirrel.
Unknown
random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "+")
The squirrel does not visit the squirrel.
Unknown
inv-random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "-")
The cat needs the squirrel.
Unknown
random
[@0: The cat needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "squirrel" "+")
@0: The bear is blue.[(triple1)] The bear is young.[(triple2)] The bear likes the cat.[(triple3)] The bear needs the rabbit.[(triple4)] The bear visits the rabbit.[(triple5)] The bear visits the squirrel.[(triple6)] The cat is blue.[(triple7)] The cat is red.[(triple8)] The cat needs the bear.[(triple9)] The rabbit likes the cat.[(triple10)] The rabbit likes the squirrel.[(triple11)] The rabbit visits the bear.[(triple12)] The squirrel is blue.[(triple13)] The squirrel is young.[(triple14)] The squirrel visits the rabbit.[(triple15)] @1: The bear visits the cat.[(((triple2 triple4) -> rule1))] The cat is round.[(((triple8) -> rule3) OR ((triple2 triple3) -> rule2))] The rabbit needs the cat.[(((triple15) -> rule6) OR ((triple5) -> rule6) OR ((((((triple8) -> rule3)) -> rule5)) -> rule6) OR ((((((triple2 triple3) -> rule2)) -> rule5)) -> rule6))] @2: The cat visits the rabbit.[(((((triple8) -> rule3)) -> rule5) OR ((((triple2 triple3) -> rule2)) -> rule5))]
The bear is blue.
("bear" "is" "blue" "+")
triple1
The bear is young.
("bear" "is" "young" "+")
triple2
The bear likes the cat.
("bear" "likes" "cat" "+")
triple3
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
triple4
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
triple5
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
triple6
The cat is blue.
("cat" "is" "blue" "+")
triple7
The cat is red.
("cat" "is" "red" "+")
triple8
The cat needs the bear.
("cat" "needs" "bear" "+")
triple9
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
triple10
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
triple11
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
triple12
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple13
The squirrel is young.
("squirrel" "is" "young" "+")
triple14
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
triple15
The bear visits the cat.
("bear" "visits" "cat" "+")
((triple2 triple4) -> (rule1 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1
The cat is round.
("cat" "is" "round" "+")
((triple8) -> (rule3 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
((triple2 triple3) -> (rule2 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
((triple15) -> (rule6 % int1))
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int1
((triple5) -> (rule6 % int1))
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int1
((((((triple8) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
((((((triple2 triple3) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
((((triple8) -> (rule3 % int2))) -> (rule5 % int1))
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
((((triple2 triple3) -> (rule2 % int2))) -> (rule5 % int1))
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2