The cat sees the dog. The cat sees the squirrel. The cat does not visit the rabbit. The dog does not eat the squirrel. The dog is young. The rabbit is nice. The rabbit sees the squirrel. The squirrel is nice. The squirrel visits the cat. The squirrel visits the dog. If the dog eats the squirrel and the dog is not rough then the dog is not big. If something is nice then it sees the dog. If something is nice then it sees the rabbit.
The cat sees the dog.
("cat" "sees" "dog" "+")
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
The cat does not visit the rabbit.
("cat" "visits" "rabbit" "-")
The dog does not eat the squirrel.
("dog" "eats" "squirrel" "-")
The dog is young.
("dog" "is" "young" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
If the dog eats the squirrel and the dog is not rough then the dog is not big.
((("dog" "eats" "squirrel" "+") ("dog" "is" "rough" "~")) -> ("dog" "is" "big" "-"))
If something is nice then it sees the dog.
((("something" "is" "nice" "+")) -> ("something" "sees" "dog" "+"))
If something is nice then it sees the rabbit.
((("something" "is" "nice" "+")) -> ("something" "sees" "rabbit" "+"))
The cat sees the dog.
True
1
proof
[(triple1)]
("cat" "sees" "dog" "+")
triple1
The squirrel is not nice.
False
1
inv-proof
[(triple8)]
("squirrel" "is" "nice" "-")
triple8
The rabbit sees the dog.
True
2
proof
[(((triple6) -> rule2))]
("rabbit" "sees" "dog" "+")
((triple6) -> (rule2 % int1))
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int1
The rabbit does not see the rabbit.
False
2
inv-proof
[(((triple6) -> rule3))]
("rabbit" "sees" "rabbit" "-")
((triple6) -> (rule3 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The dog does not see the dog.
Unknown
inv-rconc
[@1: The dog sees the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "sees" "dog" "-")
The dog sees the rabbit.
Unknown
rconc
[@1: The dog sees the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "sees" "rabbit" "+")
The rabbit does not visit the cat.
Unknown
inv-random
[@0: The rabbit visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "cat" "-")
The cat is big.
Unknown
random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "+")
@0: The cat does not visit the rabbit.[(triple3)] The cat sees the dog.[(triple1)] The cat sees the squirrel.[(triple2)] The dog does not eat the squirrel.[(triple4)] The dog is young.[(triple5)] The rabbit is nice.[(triple6)] The rabbit sees the squirrel.[(triple7)] The squirrel is nice.[(triple8)] The squirrel visits the cat.[(triple9)] The squirrel visits the dog.[(triple10)] @1: The rabbit sees the dog.[(((triple6) -> rule2))] The rabbit sees the rabbit.[(((triple6) -> rule3))] The squirrel sees the dog.[(((triple8) -> rule2))] The squirrel sees the rabbit.[(((triple8) -> rule3))]
The cat does not visit the rabbit.
("cat" "visits" "rabbit" "-")
triple3
The cat sees the dog.
("cat" "sees" "dog" "+")
triple1
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
triple2
The dog does not eat the squirrel.
("dog" "eats" "squirrel" "-")
triple4
The dog is young.
("dog" "is" "young" "+")
triple5
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple6
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
triple7
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple8
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
triple9
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
triple10
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
((triple6) -> (rule2 % int1))
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
((triple6) -> (rule3 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
((triple8) -> (rule2 % int1))
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
int1
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
((triple8) -> (rule3 % int1))
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int1