The dog is nice. The dog needs the squirrel. The dog sees the rabbit. The dog visits the rabbit. The dog visits the squirrel. The rabbit is kind. The rabbit is young. The rabbit needs the dog. The rabbit visits the dog. The rabbit visits the squirrel. The squirrel is young. The squirrel needs the dog. The squirrel needs the rabbit. The squirrel sees the dog. The squirrel sees the rabbit. The squirrel visits the rabbit. If someone visits the dog and they see the rabbit then the rabbit is cold. If someone visits the dog then the dog needs the rabbit. If someone is young then they see the dog. If someone needs the rabbit then they visit the dog. If someone sees the rabbit then they are cold. If someone sees the rabbit and the rabbit is green then the rabbit visits the squirrel.
The dog is nice.
("dog" "is" "nice" "+")
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
If someone visits the dog and they see the rabbit then the rabbit is cold.
((("someone" "visits" "dog" "+") ("someone" "sees" "rabbit" "+")) -> ("rabbit" "is" "cold" "+"))
If someone visits the dog then the dog needs the rabbit.
((("someone" "visits" "dog" "+")) -> ("dog" "needs" "rabbit" "+"))
If someone is young then they see the dog.
((("someone" "is" "young" "+")) -> ("someone" "sees" "dog" "+"))
If someone needs the rabbit then they visit the dog.
((("someone" "needs" "rabbit" "+")) -> ("someone" "visits" "dog" "+"))
If someone sees the rabbit then they are cold.
((("someone" "sees" "rabbit" "+")) -> ("someone" "is" "cold" "+"))
If someone sees the rabbit and the rabbit is green then the rabbit visits the squirrel.
((("someone" "sees" "rabbit" "+") ("rabbit" "is" "green" "+")) -> ("rabbit" "visits" "squirrel" "+"))
The rabbit needs the dog.
True
1
proof
[(triple8)]
("rabbit" "needs" "dog" "+")
triple8
The squirrel does not see the rabbit.
False
1
inv-proof
[(triple15)]
("squirrel" "sees" "rabbit" "-")
triple15
The squirrel is cold.
True
2
proof
[(((triple15) -> rule5))]
("squirrel" "is" "cold" "+")
((triple15) -> (rule5 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The rabbit does not see the dog.
False
2
inv-proof
[(((triple7) -> rule3))]
("rabbit" "sees" "dog" "-")
((triple7) -> (rule3 % int1))
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int1
The rabbit is cold.
True
4
proof
[(((((triple13) -> rule4) triple15) -> rule1) OR ((((((triple9) -> rule2)) -> rule4) triple3) -> rule1) OR ((((((((triple13) -> rule4)) -> rule2)) -> rule4) triple3) -> rule1))]
("rabbit" "is" "cold" "+")
((((triple13) -> (rule4 % int2)) triple15) -> (rule1 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int2
((((((triple9) -> (rule2 % int3))) -> (rule4 % int2)) triple3) -> (rule1 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int3
((((((((triple13) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule4 % int2)) triple3) -> (rule1 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int3
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int4
The dog does not visit the dog.
False
3
inv-proof
[(((((triple9) -> rule2)) -> rule4) OR ((((((triple13) -> rule4)) -> rule2)) -> rule4))]
("dog" "visits" "dog" "-")
((((triple9) -> (rule2 % int2))) -> (rule4 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int2
((((((triple13) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int2
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int3
The dog does not see the dog.
Unknown
inv-rconc
[@1: The dog sees the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "sees" "dog" "-")
The squirrel is nice.
Unknown
random
[@0: The squirrel is nice.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "nice" "+")
The dog is not young.
Unknown
inv-random
[@0: The dog is young.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "young" "-")
The squirrel visits the squirrel.
Unknown
random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "+")
The rabbit does not visit the rabbit.
Unknown
inv-random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "-")
The squirrel sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
@0: The dog is nice.[(triple1)] The dog needs the squirrel.[(triple2)] The dog sees the rabbit.[(triple3)] The dog visits the rabbit.[(triple4)] The dog visits the squirrel.[(triple5)] The rabbit is kind.[(triple6)] The rabbit is young.[(triple7)] The rabbit needs the dog.[(triple8)] The rabbit visits the dog.[(triple9)] The rabbit visits the squirrel.[(triple10)] The squirrel is young.[(triple11)] The squirrel needs the dog.[(triple12)] The squirrel needs the rabbit.[(triple13)] The squirrel sees the dog.[(triple14 OR ((triple11) -> rule3))] The squirrel sees the rabbit.[(triple15)] The squirrel visits the rabbit.[(triple16)] @1: The dog is cold.[(((triple3) -> rule5))] The dog needs the rabbit.[(((triple9) -> rule2) OR ((((triple13) -> rule4)) -> rule2))] The rabbit sees the dog.[(((triple7) -> rule3))] The squirrel is cold.[(((triple15) -> rule5))] The squirrel visits the dog.[(((triple13) -> rule4))] @2: The dog visits the dog.[(((((triple9) -> rule2)) -> rule4) OR ((((((triple13) -> rule4)) -> rule2)) -> rule4))] The rabbit is cold.[(((((triple13) -> rule4) triple15) -> rule1) OR ((((((triple9) -> rule2)) -> rule4) triple3) -> rule1) OR ((((((((triple13) -> rule4)) -> rule2)) -> rule4) triple3) -> rule1))]
The dog is nice.
("dog" "is" "nice" "+")
triple1
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
triple2
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
triple3
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
triple4
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
triple5
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple6
The rabbit is young.
("rabbit" "is" "young" "+")
triple7
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple8
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
triple9
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
triple10
The squirrel is young.
("squirrel" "is" "young" "+")
triple11
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
triple12
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
triple13
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
triple14
((triple11) -> (rule3 % int1))
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
int1
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
triple15
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
triple16
The dog is cold.
("dog" "is" "cold" "+")
((triple3) -> (rule5 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
((triple9) -> (rule2 % int1))
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int1
((((triple13) -> (rule4 % int2))) -> (rule2 % int1))
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int1
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int2
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
((triple7) -> (rule3 % int1))
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
((triple15) -> (rule5 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
((triple13) -> (rule4 % int1))
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
((((triple9) -> (rule2 % int2))) -> (rule4 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int2
((((((triple13) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int2
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int3
The rabbit is cold.
("rabbit" "is" "cold" "+")
((((triple13) -> (rule4 % int2)) triple15) -> (rule1 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int2
((((((triple9) -> (rule2 % int3))) -> (rule4 % int2)) triple3) -> (rule1 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int3
((((((((triple13) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule4 % int2)) triple3) -> (rule1 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int3
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int4