The bear sees the rabbit. The cow is blue. The rabbit is round. The squirrel visits the rabbit. If the cow sees the squirrel then the squirrel is young. If something is kind then it likes the bear. If something is young and it likes the squirrel then it likes the cow. If something is blue then it sees the squirrel. If something sees the bear then the bear visits the cow. If something is blue and it sees the squirrel then the squirrel sees the bear.
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
The cow is blue.
("cow" "is" "blue" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
If the cow sees the squirrel then the squirrel is young.
((("cow" "sees" "squirrel" "+")) -> ("squirrel" "is" "young" "+"))
If something is kind then it likes the bear.
((("something" "is" "kind" "+")) -> ("something" "likes" "bear" "+"))
If something is young and it likes the squirrel then it likes the cow.
((("something" "is" "young" "+") ("something" "likes" "squirrel" "+")) -> ("something" "likes" "cow" "+"))
If something is blue then it sees the squirrel.
((("something" "is" "blue" "+")) -> ("something" "sees" "squirrel" "+"))
If something sees the bear then the bear visits the cow.
((("something" "sees" "bear" "+")) -> ("bear" "visits" "cow" "+"))
If something is blue and it sees the squirrel then the squirrel sees the bear.
((("something" "is" "blue" "+") ("something" "sees" "squirrel" "+")) -> ("squirrel" "sees" "bear" "+"))
The rabbit is round.
True
1
proof
[(triple3)]
("rabbit" "is" "round" "+")
triple3
The cow is not blue.
False
1
inv-proof
[(triple2)]
("cow" "is" "blue" "-")
triple2
The cow sees the squirrel.
True
2
proof
[(((triple2) -> rule4))]
("cow" "sees" "squirrel" "+")
((triple2) -> (rule4 % int1))
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int1
The cow does not see the squirrel.
False
2
inv-proof
[(((triple2) -> rule4))]
("cow" "sees" "squirrel" "-")
((triple2) -> (rule4 % int1))
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int1
The squirrel is young.
True
3
proof
[(((((triple2) -> rule4)) -> rule1))]
("squirrel" "is" "young" "+")
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int2
The squirrel does not see the bear.
False
4
inv-proof
[(((triple2 ((triple2) -> rule4)) -> rule6))]
("squirrel" "sees" "bear" "-")
((triple2 ((triple2) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
int1
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int2
The bear visits the cow.
True
5
proof
[(((((triple2 ((triple2) -> rule4)) -> rule6)) -> rule5))]
("bear" "visits" "cow" "+")
((((triple2 ((triple2) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The bear visits the cow.
("bear" "visits" "cow" "+")
int1
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
int2
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int3
The bear does not visit the cow.
False
5
inv-proof
[(((((triple2 ((triple2) -> rule4)) -> rule6)) -> rule5))]
("bear" "visits" "cow" "-")
((((triple2 ((triple2) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The bear visits the cow.
("bear" "visits" "cow" "+")
int1
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
int2
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int3
The cow does not like the cow.
Unknown
inv-rconc
[@1: The cow likes the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "likes" "cow" "-")
The bear likes the cow.
Unknown
rconc
[@1: The bear likes the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "likes" "cow" "+")
The squirrel does not see the squirrel.
Unknown
inv-rconc
[@1: The squirrel sees the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "sees" "squirrel" "-")
The bear likes the bear.
Unknown
rconc
[@1: The bear likes the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "likes" "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 bear is young.
Unknown
random
[@0: The bear is young.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "young" "+")
The rabbit does not see the rabbit.
Unknown
inv-random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "-")
The cow is round.
Unknown
random
[@0: The cow is round.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "round" "+")
@0: The bear sees the rabbit.[(triple1)] The cow is blue.[(triple2)] The rabbit is round.[(triple3)] The squirrel visits the rabbit.[(triple4)] @1: The cow sees the squirrel.[(((triple2) -> rule4))] @2: The squirrel is young.[(((((triple2) -> rule4)) -> rule1))] The squirrel sees the bear.[(((triple2 ((triple2) -> rule4)) -> rule6))] @3: The bear visits the cow.[(((((triple2 ((triple2) -> rule4)) -> rule6)) -> rule5))]
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
triple1
The cow is blue.
("cow" "is" "blue" "+")
triple2
The rabbit is round.
("rabbit" "is" "round" "+")
triple3
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
triple4
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
((triple2) -> (rule4 % int1))
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int2
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
((triple2 ((triple2) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
int1
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int2
The bear visits the cow.
("bear" "visits" "cow" "+")
((((triple2 ((triple2) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The bear visits the cow.
("bear" "visits" "cow" "+")
int1
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
int2
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int3