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