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