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