The bear does not need the mouse. The cat needs the bear. The cow is rough. The mouse needs the cat. If the bear visits the cat then the bear needs the cow. If the bear is rough and the bear likes the cow then the cow does not need the mouse. If someone needs the bear then the bear visits the cat. If someone needs the cow then they need the bear. If someone likes the bear then the bear likes the mouse. If someone visits the bear then the bear is blue.
The bear does not need the mouse.
("bear" "needs" "mouse" "-")
The cat needs the bear.
("cat" "needs" "bear" "+")
The cow is rough.
("cow" "is" "rough" "+")
The mouse needs the cat.
("mouse" "needs" "cat" "+")
If the bear visits the cat then the bear needs the cow.
((("bear" "visits" "cat" "+")) -> ("bear" "needs" "cow" "+"))
If the bear is rough and the bear likes the cow then the cow does not need the mouse.
((("bear" "is" "rough" "+") ("bear" "likes" "cow" "+")) -> ("cow" "needs" "mouse" "-"))
If someone needs the bear then the bear visits the cat.
((("someone" "needs" "bear" "+")) -> ("bear" "visits" "cat" "+"))
If someone needs the cow then they need the bear.
((("someone" "needs" "cow" "+")) -> ("someone" "needs" "bear" "+"))
If someone likes the bear then the bear likes the mouse.
((("someone" "likes" "bear" "+")) -> ("bear" "likes" "mouse" "+"))
If someone visits the bear then the bear is blue.
((("someone" "visits" "bear" "+")) -> ("bear" "is" "blue" "+"))
The cow is rough.
True
1
proof
[(triple3)]
("cow" "is" "rough" "+")
triple3
The bear needs the mouse.
False
1
inv-proof
[(triple1)]
("bear" "needs" "mouse" "+")
triple1
The bear visits the cat.
True
2
proof
[(((triple2) -> rule3))]
("bear" "visits" "cat" "+")
((triple2) -> (rule3 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1
The bear does not visit the cat.
False
2
inv-proof
[(((triple2) -> rule3))]
("bear" "visits" "cat" "-")
((triple2) -> (rule3 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1
The bear needs the cow.
True
3
proof
[(((((triple2) -> rule3)) -> rule1))]
("bear" "needs" "cow" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The bear needs the cow.
("bear" "needs" "cow" "+")
int1
The bear visits the cat.
("bear" "visits" "cat" "+")
int2
The bear does not need the cow.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule1))]
("bear" "needs" "cow" "-")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The bear needs the cow.
("bear" "needs" "cow" "+")
int1
The bear visits the cat.
("bear" "visits" "cat" "+")
int2
The bear needs the bear.
True
4
proof
[(((((((triple2) -> rule3)) -> rule1)) -> rule4))]
("bear" "needs" "bear" "+")
((((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear needs the cow.
("bear" "needs" "cow" "+")
int2
The bear visits the cat.
("bear" "visits" "cat" "+")
int3
The bear does not need the bear.
False
4
inv-proof
[(((((((triple2) -> rule3)) -> rule1)) -> rule4))]
("bear" "needs" "bear" "-")
((((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear needs the cow.
("bear" "needs" "cow" "+")
int2
The bear visits the cat.
("bear" "visits" "cat" "+")
int3
The bear does not like the mouse.
Unknown
inv-rconc
[@1: The bear likes the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "likes" "mouse" "-")
The mouse needs the bear.
Unknown
rconc
[@1: The mouse needs the bear.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "needs" "bear" "+")
The cow does not need the bear.
Unknown
inv-rconc
[@1: The cow needs the bear.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "needs" "bear" "-")
The bear is blue.
Unknown
rconc
[@1: The bear is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "is" "blue" "+")
The bear does not like the bear.
Unknown
inv-random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "-")
The cat needs the mouse.
Unknown
random
[@0: The cat needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "mouse" "+")
The cat is not round.
Unknown
inv-random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
@0: The bear does not need the mouse.[(triple1)] The cat needs the bear.[(triple2)] The cow is rough.[(triple3)] The mouse needs the cat.[(triple4)] @1: The bear visits the cat.[(((triple2) -> rule3))] @2: The bear needs the cow.[(((((triple2) -> rule3)) -> rule1))] @3: The bear needs the bear.[(((((((triple2) -> rule3)) -> rule1)) -> rule4))]
The bear does not need the mouse.
("bear" "needs" "mouse" "-")
triple1
The cat needs the bear.
("cat" "needs" "bear" "+")
triple2
The cow is rough.
("cow" "is" "rough" "+")
triple3
The mouse needs the cat.
("mouse" "needs" "cat" "+")
triple4
The bear visits the cat.
("bear" "visits" "cat" "+")
((triple2) -> (rule3 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1
The bear needs the cow.
("bear" "needs" "cow" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The bear needs the cow.
("bear" "needs" "cow" "+")
int1
The bear visits the cat.
("bear" "visits" "cat" "+")
int2
The bear needs the bear.
("bear" "needs" "bear" "+")
((((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear needs the cow.
("bear" "needs" "cow" "+")
int2
The bear visits the cat.
("bear" "visits" "cat" "+")
int3