The dog likes the rabbit. The dog needs the rabbit. The rabbit chases the dog. The rabbit is big. The rabbit is young. The rabbit likes the squirrel. The rabbit needs the squirrel. The squirrel chases the dog. The squirrel is green. The squirrel is kind. If something needs the squirrel and it chases the squirrel then it likes the squirrel. If something chases the rabbit then the rabbit is green. If something needs the dog then the dog chases the squirrel. If something chases the dog and the dog is big then it chases the squirrel. If something needs the rabbit then it chases the rabbit. If something is green then it chases the rabbit.
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
If something needs the squirrel and it chases the squirrel then it likes the squirrel.
((("something" "needs" "squirrel" "+") ("something" "chases" "squirrel" "+")) -> ("something" "likes" "squirrel" "+"))
If something chases the rabbit then the rabbit is green.
((("something" "chases" "rabbit" "+")) -> ("rabbit" "is" "green" "+"))
If something needs the dog then the dog chases the squirrel.
((("something" "needs" "dog" "+")) -> ("dog" "chases" "squirrel" "+"))
If something chases the dog and the dog is big then it chases the squirrel.
((("something" "chases" "dog" "+") ("dog" "is" "big" "+")) -> ("something" "chases" "squirrel" "+"))
If something needs the rabbit then it chases the rabbit.
((("something" "needs" "rabbit" "+")) -> ("something" "chases" "rabbit" "+"))
If something is green then it chases the rabbit.
((("something" "is" "green" "+")) -> ("something" "chases" "rabbit" "+"))
The rabbit chases the dog.
True
1
proof
[(triple3)]
("rabbit" "chases" "dog" "+")
triple3
The rabbit does not need the squirrel.
False
1
inv-proof
[(triple7)]
("rabbit" "needs" "squirrel" "-")
triple7
The dog chases the rabbit.
True
2
proof
[(((triple2) -> rule5))]
("dog" "chases" "rabbit" "+")
((triple2) -> (rule5 % int1))
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int1
The squirrel does not chase the rabbit.
False
2
inv-proof
[(((triple9) -> rule6))]
("squirrel" "chases" "rabbit" "-")
((triple9) -> (rule6 % int1))
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
int1
The rabbit is green.
True
3
proof
[(((((triple2) -> rule5)) -> rule2) OR ((((triple9) -> rule6)) -> rule2))]
("rabbit" "is" "green" "+")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int2
((((triple9) -> (rule6 % int2))) -> (rule2 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
int2
The rabbit is not green.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule2) OR ((((triple9) -> rule6)) -> rule2))]
("rabbit" "is" "green" "-")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int2
((((triple9) -> (rule6 % int2))) -> (rule2 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
int2
The rabbit chases the rabbit.
True
4
proof
[(((((((triple2) -> rule5)) -> rule2)) -> rule6) OR ((((((triple9) -> rule6)) -> rule2)) -> rule6))]
("rabbit" "chases" "rabbit" "+")
((((((triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int3
((((((triple9) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
int3
The rabbit does not chase the rabbit.
False
4
inv-proof
[(((((((triple2) -> rule5)) -> rule2)) -> rule6) OR ((((((triple9) -> rule6)) -> rule2)) -> rule6))]
("rabbit" "chases" "rabbit" "-")
((((((triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int3
((((((triple9) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
int3
The squirrel does not like the squirrel.
Unknown
inv-rconc
[@1: The squirrel likes the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "likes" "squirrel" "-")
The dog chases the squirrel.
Unknown
rconc
[@1: The dog chases the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "chases" "squirrel" "+")
The dog does not like the squirrel.
Unknown
inv-rconc
[@1: The dog likes the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "likes" "squirrel" "-")
The squirrel chases the squirrel.
Unknown
rconc
[@1: The squirrel chases the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "chases" "squirrel" "+")
The rabbit does not need the rabbit.
Unknown
inv-random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "-")
The squirrel is round.
Unknown
random
[@0: The squirrel is round.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "round" "+")
The squirrel is not big.
Unknown
inv-random
[@0: The squirrel is big.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "big" "-")
The rabbit is round.
Unknown
random
[@0: The rabbit is round.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "round" "+")
@0: The dog likes the rabbit.[(triple1)] The dog needs the rabbit.[(triple2)] The rabbit chases the dog.[(triple3)] The rabbit is big.[(triple4)] The rabbit is young.[(triple5)] The rabbit likes the squirrel.[(triple6)] The rabbit needs the squirrel.[(triple7)] The squirrel chases the dog.[(triple8)] The squirrel is green.[(triple9)] The squirrel is kind.[(triple10)] @1: The dog chases the rabbit.[(((triple2) -> rule5))] The squirrel chases the rabbit.[(((triple9) -> rule6))] @2: The rabbit is green.[(((((triple2) -> rule5)) -> rule2) OR ((((triple9) -> rule6)) -> rule2))] @3: The rabbit chases the rabbit.[(((((((triple2) -> rule5)) -> rule2)) -> rule6) OR ((((((triple9) -> rule6)) -> rule2)) -> rule6))]
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
triple1
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
triple2
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
triple3
The rabbit is big.
("rabbit" "is" "big" "+")
triple4
The rabbit is young.
("rabbit" "is" "young" "+")
triple5
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
triple6
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
triple7
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
triple8
The squirrel is green.
("squirrel" "is" "green" "+")
triple9
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple10
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
((triple2) -> (rule5 % int1))
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int1
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
((triple9) -> (rule6 % int1))
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int2
((((triple9) -> (rule6 % int2))) -> (rule2 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
int2
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
((((((triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int3
((((((triple9) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
int3