The cow needs the squirrel. The rabbit is nice. The squirrel eats the cow. If something needs the cow then the cow likes the rabbit. If something needs the squirrel then it needs the cow. If something needs the squirrel and it does not like the cow then it is big.
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
If something needs the cow then the cow likes the rabbit.
((("something" "needs" "cow" "+")) -> ("cow" "likes" "rabbit" "+"))
If something needs the squirrel then it needs the cow.
((("something" "needs" "squirrel" "+")) -> ("something" "needs" "cow" "+"))
If something needs the squirrel and it does not like the cow then it is big.
((("something" "needs" "squirrel" "+") ("something" "likes" "cow" "~")) -> ("something" "is" "big" "+"))
The cow needs the squirrel.
True
1
proof
[(triple1)]
("cow" "needs" "squirrel" "+")
triple1
The squirrel does not eat the cow.
False
1
inv-proof
[(triple3)]
("squirrel" "eats" "cow" "-")
triple3
The cow needs the cow.
True
2
proof
[(((triple1) -> rule2))]
("cow" "needs" "cow" "+")
((triple1) -> (rule2 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow does not need the cow.
False
2
inv-proof
[(((triple1) -> rule2))]
("cow" "needs" "cow" "-")
((triple1) -> (rule2 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow likes the rabbit.
True
3
proof
[(((((triple1) -> rule2)) -> rule1))]
("cow" "likes" "rabbit" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow does not like the rabbit.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule1))]
("cow" "likes" "rabbit" "-")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The rabbit does not need the cow.
Unknown
inv-rconc
[@1: The rabbit needs the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "needs" "cow" "-")
The rabbit is big.
Unknown
rconc
[@1: The rabbit is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "is" "big" "+")
The cow is not big.
Unknown
inv-rconc
[@1: The cow is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "is" "big" "-")
The rabbit is young.
Unknown
random
[@0: The rabbit is young.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "young" "+")
The cow does not eat the squirrel.
Unknown
inv-random
[@0: The cow eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "squirrel" "-")
The rabbit likes the rabbit.
Unknown
random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "+")
@0: The cow needs the squirrel.[(triple1)] The rabbit is nice.[(triple2)] The squirrel eats the cow.[(triple3)] @1: The cow needs the cow.[(((triple1) -> rule2))] @2: The cow likes the rabbit.[(((((triple1) -> rule2)) -> rule1))]
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
triple1
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple2
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
triple3
The cow needs the cow.
("cow" "needs" "cow" "+")
((triple1) -> (rule2 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2