The bear is blue. The bear needs the squirrel. The bear sees the cat. The cat is rough. The cat needs the bear. The cat needs the rabbit. The rabbit is blue. The rabbit is green. The rabbit is rough. The squirrel is kind. If the cat needs the rabbit and the rabbit is kind then the cat is young. If something is blue then it sees the rabbit. If something sees the rabbit then it is kind. If something is green then it needs the cat. If something needs the rabbit and the rabbit chases the squirrel then it chases the squirrel. If something is young then it sees the rabbit. If something is blue then it chases the squirrel.
The bear is blue.
("bear" "is" "blue" "+")
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
The bear sees the cat.
("bear" "sees" "cat" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat needs the bear.
("cat" "needs" "bear" "+")
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
If the cat needs the rabbit and the rabbit is kind then the cat is young.
((("cat" "needs" "rabbit" "+") ("rabbit" "is" "kind" "+")) -> ("cat" "is" "young" "+"))
If something is blue then it sees the rabbit.
((("something" "is" "blue" "+")) -> ("something" "sees" "rabbit" "+"))
If something sees the rabbit then it is kind.
((("something" "sees" "rabbit" "+")) -> ("something" "is" "kind" "+"))
If something is green then it needs the cat.
((("something" "is" "green" "+")) -> ("something" "needs" "cat" "+"))
If something needs the rabbit and the rabbit chases the squirrel then it chases the squirrel.
((("something" "needs" "rabbit" "+") ("rabbit" "chases" "squirrel" "+")) -> ("something" "chases" "squirrel" "+"))
If something is young then it sees the rabbit.
((("something" "is" "young" "+")) -> ("something" "sees" "rabbit" "+"))
If something is blue then it chases the squirrel.
((("something" "is" "blue" "+")) -> ("something" "chases" "squirrel" "+"))
The rabbit is blue.
True
1
proof
[(triple7)]
("rabbit" "is" "blue" "+")
triple7
The cat does not need the bear.
False
1
inv-proof
[(triple5)]
("cat" "needs" "bear" "-")
triple5
The bear sees the rabbit.
True
2
proof
[(((triple1) -> rule2))]
("bear" "sees" "rabbit" "+")
((triple1) -> (rule2 % int1))
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int1
The rabbit does not see the rabbit.
False
2
inv-proof
[(((triple7) -> rule2))]
("rabbit" "sees" "rabbit" "-")
((triple7) -> (rule2 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit is kind.
True
3
proof
[(((((triple7) -> rule2)) -> rule3))]
("rabbit" "is" "kind" "+")
((((triple7) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int2
The bear is not kind.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule3))]
("bear" "is" "kind" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int2
The cat is young.
True
5
proof
[(((triple6 ((((triple7) -> rule2)) -> rule3)) -> rule1))]
("cat" "is" "young" "+")
((triple6 ((((triple7) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int3
The cat is not young.
False
5
inv-proof
[(((triple6 ((((triple7) -> rule2)) -> rule3)) -> rule1))]
("cat" "is" "young" "-")
((triple6 ((((triple7) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int3
The cat sees the rabbit.
True
6
proof
[(((((triple6 ((((triple7) -> rule2)) -> rule3)) -> rule1)) -> rule6))]
("cat" "sees" "rabbit" "+")
((((triple6 ((((triple7) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The rabbit is kind.
("rabbit" "is" "kind" "+")
int3
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int4
The cat does not see the rabbit.
False
6
inv-proof
[(((((triple6 ((((triple7) -> rule2)) -> rule3)) -> rule1)) -> rule6))]
("cat" "sees" "rabbit" "-")
((((triple6 ((((triple7) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The rabbit is kind.
("rabbit" "is" "kind" "+")
int3
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int4
The cat is kind.
True
7
proof
[(((((((triple6 ((((triple7) -> rule2)) -> rule3)) -> rule1)) -> rule6)) -> rule3))]
("cat" "is" "kind" "+")
((((((triple6 ((((triple7) -> (rule2 % int5))) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int2
The cat is young.
("cat" "is" "young" "+")
int3
The rabbit is kind.
("rabbit" "is" "kind" "+")
int4
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int5
The cat is not kind.
False
7
inv-proof
[(((((((triple6 ((((triple7) -> rule2)) -> rule3)) -> rule1)) -> rule6)) -> rule3))]
("cat" "is" "kind" "-")
((((((triple6 ((((triple7) -> (rule2 % int5))) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int2
The cat is young.
("cat" "is" "young" "+")
int3
The rabbit is kind.
("rabbit" "is" "kind" "+")
int4
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int5
The squirrel does not need the cat.
Unknown
inv-rconc
[@1: The squirrel needs the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "needs" "cat" "-")
The squirrel sees the rabbit.
Unknown
rconc
[@1: The squirrel sees the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "sees" "rabbit" "+")
The squirrel does not chase the squirrel.
Unknown
inv-rconc
[@1: The squirrel chases the squirrel.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "chases" "squirrel" "-")
The bear needs the cat.
Unknown
rconc
[@1: The bear needs the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "needs" "cat" "+")
The cat does not need the cat.
Unknown
inv-rconc
[@1: The cat needs the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "needs" "cat" "-")
The rabbit sees the cat.
Unknown
random
[@0: The rabbit sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "cat" "+")
The rabbit does not need the squirrel.
Unknown
inv-random
[@0: The rabbit needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "squirrel" "-")
The squirrel sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
The cat does not chase the rabbit.
Unknown
inv-random
[@0: The cat chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "rabbit" "-")
The rabbit chases the rabbit.
Unknown
random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "+")
The bear does not chase the bear.
Unknown
inv-random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "-")
The squirrel sees the cat.
Unknown
random
[@0: The squirrel sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "cat" "+")
@0: The bear is blue.[(triple1)] The bear needs the squirrel.[(triple2)] The bear sees the cat.[(triple3)] The cat is rough.[(triple4)] The cat needs the bear.[(triple5)] The cat needs the rabbit.[(triple6)] The rabbit is blue.[(triple7)] The rabbit is green.[(triple8)] The rabbit is rough.[(triple9)] The squirrel is kind.[(triple10)] @1: The bear chases the squirrel.[(((triple1) -> rule7))] The bear sees the rabbit.[(((triple1) -> rule2))] The rabbit chases the squirrel.[(((triple7) -> rule7))] The rabbit needs the cat.[(((triple8) -> rule4))] The rabbit sees the rabbit.[(((triple7) -> rule2))] @2: The bear is kind.[(((((triple1) -> rule2)) -> rule3))] The cat chases the squirrel.[(((triple6 ((triple7) -> rule7)) -> rule5))] The rabbit is kind.[(((((triple7) -> rule2)) -> rule3))] @3: The cat is young.[(((triple6 ((((triple7) -> rule2)) -> rule3)) -> rule1))] @4: The cat sees the rabbit.[(((((triple6 ((((triple7) -> rule2)) -> rule3)) -> rule1)) -> rule6))] @5: The cat is kind.[(((((((triple6 ((((triple7) -> rule2)) -> rule3)) -> rule1)) -> rule6)) -> rule3))]
The bear is blue.
("bear" "is" "blue" "+")
triple1
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
triple2
The bear sees the cat.
("bear" "sees" "cat" "+")
triple3
The cat is rough.
("cat" "is" "rough" "+")
triple4
The cat needs the bear.
("cat" "needs" "bear" "+")
triple5
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
triple6
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple7
The rabbit is green.
("rabbit" "is" "green" "+")
triple8
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple9
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple10
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
((triple1) -> (rule7 % int1))
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
int1
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
((triple1) -> (rule2 % int1))
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int1
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
((triple7) -> (rule7 % int1))
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
int1
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
((triple8) -> (rule4 % int1))
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
((triple7) -> (rule2 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The bear is kind.
("bear" "is" "kind" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int2
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
((triple6 ((triple7) -> (rule7 % int2))) -> (rule5 % int1))
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
int1
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
int2
The rabbit is kind.
("rabbit" "is" "kind" "+")
((((triple7) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int2
The cat is young.
("cat" "is" "young" "+")
((triple6 ((((triple7) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int3
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
((((triple6 ((((triple7) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The rabbit is kind.
("rabbit" "is" "kind" "+")
int3
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int4
The cat is kind.
("cat" "is" "kind" "+")
((((((triple6 ((((triple7) -> (rule2 % int5))) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int2
The cat is young.
("cat" "is" "young" "+")
int3
The rabbit is kind.
("rabbit" "is" "kind" "+")
int4
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int5