The bear is big. The bear is green. The bear likes the cat. The cat is big. The cat is blue. The cat is round. The cat likes the rabbit. The cat does not visit the bear. The rabbit is big. The rabbit does not visit the cat. If something is round then it visits the cat. Rough things are blue. If something likes the rabbit then it sees the cat. If something is rough and it does not visit the bear then it likes the rabbit. If something likes the bear and the bear is round then it does not see the rabbit. If the cat is big and the cat is round then the cat does not see the rabbit. If something sees the cat then the cat sees the bear. If something sees the cat then the cat likes the rabbit.
The bear is big.
("bear" "is" "big" "+")
The bear is green.
("bear" "is" "green" "+")
The bear likes the cat.
("bear" "likes" "cat" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is round.
("cat" "is" "round" "+")
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
The cat does not visit the bear.
("cat" "visits" "bear" "-")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit does not visit the cat.
("rabbit" "visits" "cat" "-")
If something is round then it visits the cat.
((("something" "is" "round" "+")) -> ("something" "visits" "cat" "+"))
Rough things are blue.
((("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
If something likes the rabbit then it sees the cat.
((("something" "likes" "rabbit" "+")) -> ("something" "sees" "cat" "+"))
If something is rough and it does not visit the bear then it likes the rabbit.
((("something" "is" "rough" "+") ("something" "visits" "bear" "~")) -> ("something" "likes" "rabbit" "+"))
If something likes the bear and the bear is round then it does not see the rabbit.
((("something" "likes" "bear" "+") ("bear" "is" "round" "+")) -> ("something" "sees" "rabbit" "-"))
If the cat is big and the cat is round then the cat does not see the rabbit.
((("cat" "is" "big" "+") ("cat" "is" "round" "+")) -> ("cat" "sees" "rabbit" "-"))
If something sees the cat then the cat sees the bear.
((("something" "sees" "cat" "+")) -> ("cat" "sees" "bear" "+"))
If something sees the cat then the cat likes the rabbit.
((("something" "sees" "cat" "+")) -> ("cat" "likes" "rabbit" "+"))
The bear likes the cat.
True
1
proof
[(triple3)]
("bear" "likes" "cat" "+")
triple3
The cat is not blue.
False
1
inv-proof
[(triple5)]
("cat" "is" "blue" "-")
triple5
The cat does not see the rabbit.
True
3
proof
[(((triple4 triple6) -> rule6))]
("cat" "sees" "rabbit" "-")
((triple4 triple6) -> (rule6 % int1))
The cat does not see the rabbit.
("cat" "sees" "rabbit" "-")
int1
The cat does not see the cat.
False
2
inv-proof
[(((triple7) -> rule3))]
("cat" "sees" "cat" "-")
((triple7) -> (rule3 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat sees the bear.
True
3
proof
[(((((triple7) -> rule3)) -> rule7))]
("cat" "sees" "bear" "+")
((((triple7) -> (rule3 % int2))) -> (rule7 % int1))
The cat sees the bear.
("cat" "sees" "bear" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
The cat does not see the bear.
False
3
inv-proof
[(((((triple7) -> rule3)) -> rule7))]
("cat" "sees" "bear" "-")
((((triple7) -> (rule3 % int2))) -> (rule7 % int1))
The cat sees the bear.
("cat" "sees" "bear" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
The rabbit does not see the cat.
Unknown
inv-rconc
[@2: The rabbit sees the cat.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("rabbit" "sees" "cat" "-")
The rabbit likes the rabbit.
Unknown
rconc
[@1: The rabbit likes the rabbit.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "likes" "rabbit" "+")
The bear is not blue.
Unknown
inv-rconc
[@1: The bear is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "is" "blue" "-")
The rabbit is round.
Unknown
random
[@0: The rabbit is round.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "round" "+")
The bear does not visit the bear.
Unknown
inv-random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "-")
The rabbit is rough.
Unknown
random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "+")
@0: The bear is big.[(triple1)] The bear is green.[(triple2)] The bear likes the cat.[(triple3)] The cat does not visit the bear.[(triple8)] The cat is big.[(triple4)] The cat is blue.[(triple5)] The cat is round.[(triple6)] The cat likes the rabbit.[(triple7)] The rabbit does not visit the cat.[(triple10)] The rabbit is big.[(triple9)] @1: The cat does not see the rabbit.[(((triple4 triple6) -> rule6))] The cat sees the cat.[(((triple7) -> rule3))] The cat visits the cat.[(((triple6) -> rule1))] @2: The cat sees the bear.[(((((triple7) -> rule3)) -> rule7))]
The bear is big.
("bear" "is" "big" "+")
triple1
The bear is green.
("bear" "is" "green" "+")
triple2
The bear likes the cat.
("bear" "likes" "cat" "+")
triple3
The cat does not visit the bear.
("cat" "visits" "bear" "-")
triple8
The cat is big.
("cat" "is" "big" "+")
triple4
The cat is blue.
("cat" "is" "blue" "+")
triple5
The cat is round.
("cat" "is" "round" "+")
triple6
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
triple7
The rabbit does not visit the cat.
("rabbit" "visits" "cat" "-")
triple10
The rabbit is big.
("rabbit" "is" "big" "+")
triple9
The cat does not see the rabbit.
("cat" "sees" "rabbit" "-")
((triple4 triple6) -> (rule6 % int1))
The cat does not see the rabbit.
("cat" "sees" "rabbit" "-")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
((triple7) -> (rule3 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
((triple6) -> (rule1 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat sees the bear.
("cat" "sees" "bear" "+")
((((triple7) -> (rule3 % int2))) -> (rule7 % int1))
The cat sees the bear.
("cat" "sees" "bear" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2