The bear eats the cat. The bear is green. The cat eats the bear. If someone visits the cat and the cat visits the bear then they eat the bear. If someone eats the cat then they visit the cat. If someone visits the bear and the bear visits the cat then the bear is kind. If someone visits the cat and they like the cat then they are green. If someone eats the bear then the bear likes the cat. If someone visits the cat then the cat eats the bear.
The bear eats the cat.
("bear" "eats" "cat" "+")
The bear is green.
("bear" "is" "green" "+")
The cat eats the bear.
("cat" "eats" "bear" "+")
If someone visits the cat and the cat visits the bear then they eat the bear.
((("someone" "visits" "cat" "+") ("cat" "visits" "bear" "+")) -> ("someone" "eats" "bear" "+"))
If someone eats the cat then they visit the cat.
((("someone" "eats" "cat" "+")) -> ("someone" "visits" "cat" "+"))
If someone visits the bear and the bear visits the cat then the bear is kind.
((("someone" "visits" "bear" "+") ("bear" "visits" "cat" "+")) -> ("bear" "is" "kind" "+"))
If someone visits the cat and they like the cat then they are green.
((("someone" "visits" "cat" "+") ("someone" "likes" "cat" "+")) -> ("someone" "is" "green" "+"))
If someone eats the bear then the bear likes the cat.
((("someone" "eats" "bear" "+")) -> ("bear" "likes" "cat" "+"))
If someone visits the cat then the cat eats the bear.
((("someone" "visits" "cat" "+")) -> ("cat" "eats" "bear" "+"))
The cat eats the bear.
True
1
proof
[(triple3 OR ((((triple1) -> rule2)) -> rule6))]
("cat" "eats" "bear" "+")
triple3
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The cat eats the bear.
("cat" "eats" "bear" "+")
int1
The bear visits the cat.
("bear" "visits" "cat" "+")
int2
The bear does not eat the cat.
False
1
inv-proof
[(triple1)]
("bear" "eats" "cat" "-")
triple1
The cat does not visit the cat.
Unknown
inv-rconc
[@1: The cat visits the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "visits" "cat" "-")
The bear likes the bear.
Unknown
random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "+")
@0: The bear eats the cat.[(triple1)] The bear is green.[(triple2 OR ((((triple1) -> rule2) ((triple3) -> rule5)) -> rule4) OR ((((triple1) -> rule2) ((((((triple1) -> rule2)) -> rule6)) -> rule5)) -> rule4))] The cat eats the bear.[(triple3 OR ((((triple1) -> rule2)) -> rule6))] @1: The bear likes the cat.[(((triple3) -> rule5) OR ((((((triple1) -> rule2)) -> rule6)) -> rule5))] The bear visits the cat.[(((triple1) -> rule2))]
The bear eats the cat.
("bear" "eats" "cat" "+")
triple1
The bear is green.
("bear" "is" "green" "+")
triple2
((((triple1) -> (rule2 % int3)) ((triple3) -> (rule5 % int2))) -> (rule4 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The bear likes the cat.
("bear" "likes" "cat" "+")
int2
The bear visits the cat.
("bear" "visits" "cat" "+")
int3
((((triple1) -> (rule2 % int4)) ((((((triple1) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The bear likes the cat.
("bear" "likes" "cat" "+")
int2
The cat eats the bear.
("cat" "eats" "bear" "+")
int3
The bear visits the cat.
("bear" "visits" "cat" "+")
int4
The cat eats the bear.
("cat" "eats" "bear" "+")
triple3
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The cat eats the bear.
("cat" "eats" "bear" "+")
int1
The bear visits the cat.
("bear" "visits" "cat" "+")
int2
The bear likes the cat.
("bear" "likes" "cat" "+")
((triple3) -> (rule5 % int1))
The bear likes the cat.
("bear" "likes" "cat" "+")
int1
((((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The bear likes the cat.
("bear" "likes" "cat" "+")
int1
The cat eats the bear.
("cat" "eats" "bear" "+")
int2
The bear visits the cat.
("bear" "visits" "cat" "+")
int3
The bear visits the cat.
("bear" "visits" "cat" "+")
((triple1) -> (rule2 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1