The bear visits the rabbit. The rabbit is big. The rabbit needs the bear. The squirrel eats the bear. The squirrel is rough. The squirrel is young. The squirrel needs the rabbit. If something is big then it eats the squirrel. If something is big and it needs the squirrel then the squirrel eats the bear. If something is big and it eats the squirrel then the squirrel is big.
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
If something is big then it eats the squirrel.
((("something" "is" "big" "+")) -> ("something" "eats" "squirrel" "+"))
If something is big and it needs the squirrel then the squirrel eats the bear.
((("something" "is" "big" "+") ("something" "needs" "squirrel" "+")) -> ("squirrel" "eats" "bear" "+"))
If something is big and it eats the squirrel then the squirrel is big.
((("something" "is" "big" "+") ("something" "eats" "squirrel" "+")) -> ("squirrel" "is" "big" "+"))
The rabbit needs the bear.
True
1
proof
[(triple3)]
("rabbit" "needs" "bear" "+")
triple3
The bear does not visit the rabbit.
False
1
inv-proof
[(triple1)]
("bear" "visits" "rabbit" "-")
triple1
The rabbit eats the squirrel.
True
2
proof
[(((triple2) -> rule1))]
("rabbit" "eats" "squirrel" "+")
((triple2) -> (rule1 % int1))
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int1
The rabbit does not eat the squirrel.
False
2
inv-proof
[(((triple2) -> rule1))]
("rabbit" "eats" "squirrel" "-")
((triple2) -> (rule1 % int1))
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int1
The squirrel is big.
True
4
proof
[(((triple2 ((triple2) -> rule1)) -> rule3))]
("squirrel" "is" "big" "+")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int2
The squirrel is not big.
False
4
inv-proof
[(((triple2 ((triple2) -> rule1)) -> rule3))]
("squirrel" "is" "big" "-")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int2
The squirrel eats the squirrel.
True
5
proof
[(((((triple2 ((triple2) -> rule1)) -> rule3)) -> rule1))]
("squirrel" "eats" "squirrel" "+")
((((triple2 ((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int3
The squirrel does not eat the squirrel.
False
5
inv-proof
[(((((triple2 ((triple2) -> rule1)) -> rule3)) -> rule1))]
("squirrel" "eats" "squirrel" "-")
((((triple2 ((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int3
The bear does not eat the squirrel.
Unknown
inv-rconc
[@1: The bear eats the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "eats" "squirrel" "-")
The bear is young.
Unknown
random
[@0: The bear is young.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "young" "+")
The bear is not red.
Unknown
inv-random
[@0: The bear is red.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "red" "-")
The rabbit needs the rabbit.
Unknown
random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "+")
The rabbit is not rough.
Unknown
inv-random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "-")
The bear needs the bear.
Unknown
random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "+")
The bear does not visit the squirrel.
Unknown
inv-random
[@0: The bear visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "squirrel" "-")
The rabbit is young.
Unknown
random
[@0: The rabbit is young.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "young" "+")
@0: The bear visits the rabbit.[(triple1)] The rabbit is big.[(triple2)] The rabbit needs the bear.[(triple3)] The squirrel eats the bear.[(triple4)] The squirrel is rough.[(triple5)] The squirrel is young.[(triple6)] The squirrel needs the rabbit.[(triple7)] @1: The rabbit eats the squirrel.[(((triple2) -> rule1))] @2: The squirrel is big.[(((triple2 ((triple2) -> rule1)) -> rule3))] @3: The squirrel eats the squirrel.[(((((triple2 ((triple2) -> rule1)) -> rule3)) -> rule1))]
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
triple1
The rabbit is big.
("rabbit" "is" "big" "+")
triple2
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
triple3
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
triple4
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple5
The squirrel is young.
("squirrel" "is" "young" "+")
triple6
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
triple7
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
((triple2) -> (rule1 % int1))
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int2
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
((((triple2 ((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int3