The cat sees the dog. The dog visits the cat. The mouse visits the dog. The squirrel eats the dog. If someone eats the squirrel then the squirrel eats the cat. If someone eats the dog and the dog sees the cat then they eat the cat. If someone visits the squirrel then the squirrel is cold. If someone is kind then they eat the dog. If someone visits the cat then the cat sees the dog. If someone sees the dog and the dog eats the cat then they visit the mouse. If someone visits the dog then the dog visits the squirrel. If someone eats the dog then they visit the squirrel.
The cat sees the dog.
("cat" "sees" "dog" "+")
The dog visits the cat.
("dog" "visits" "cat" "+")
The mouse visits the dog.
("mouse" "visits" "dog" "+")
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
If someone eats the squirrel then the squirrel eats the cat.
((("someone" "eats" "squirrel" "+")) -> ("squirrel" "eats" "cat" "+"))
If someone eats the dog and the dog sees the cat then they eat the cat.
((("someone" "eats" "dog" "+") ("dog" "sees" "cat" "+")) -> ("someone" "eats" "cat" "+"))
If someone visits the squirrel then the squirrel is cold.
((("someone" "visits" "squirrel" "+")) -> ("squirrel" "is" "cold" "+"))
If someone is kind then they eat the dog.
((("someone" "is" "kind" "+")) -> ("someone" "eats" "dog" "+"))
If someone visits the cat then the cat sees the dog.
((("someone" "visits" "cat" "+")) -> ("cat" "sees" "dog" "+"))
If someone sees the dog and the dog eats the cat then they visit the mouse.
((("someone" "sees" "dog" "+") ("dog" "eats" "cat" "+")) -> ("someone" "visits" "mouse" "+"))
If someone visits the dog then the dog visits the squirrel.
((("someone" "visits" "dog" "+")) -> ("dog" "visits" "squirrel" "+"))
If someone eats the dog then they visit the squirrel.
((("someone" "eats" "dog" "+")) -> ("someone" "visits" "squirrel" "+"))
The cat sees the dog.
True
1
proof
[(triple1 OR ((triple2) -> rule5))]
("cat" "sees" "dog" "+")
triple1
((triple2) -> (rule5 % int1))
The cat sees the dog.
("cat" "sees" "dog" "+")
int1
The cat does not see the dog.
False
1
inv-proof
[(triple1 OR ((triple2) -> rule5))]
("cat" "sees" "dog" "-")
triple1
((triple2) -> (rule5 % int1))
The cat sees the dog.
("cat" "sees" "dog" "+")
int1
The dog visits the squirrel.
True
2
proof
[(((triple3) -> rule7))]
("dog" "visits" "squirrel" "+")
((triple3) -> (rule7 % int1))
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int1
The dog does not visit the squirrel.
False
2
inv-proof
[(((triple3) -> rule7))]
("dog" "visits" "squirrel" "-")
((triple3) -> (rule7 % int1))
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int1
The squirrel is cold.
True
3
proof
[(((((triple3) -> rule7)) -> rule3) OR ((((triple4) -> rule8)) -> rule3))]
("squirrel" "is" "cold" "+")
((((triple3) -> (rule7 % int2))) -> (rule3 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int2
((((triple4) -> (rule8 % int2))) -> (rule3 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int2
The squirrel is not cold.
False
3
inv-proof
[(((((triple3) -> rule7)) -> rule3) OR ((((triple4) -> rule8)) -> rule3))]
("squirrel" "is" "cold" "-")
((((triple3) -> (rule7 % int2))) -> (rule3 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int2
((((triple4) -> (rule8 % int2))) -> (rule3 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int2
The cat does not visit the squirrel.
Unknown
inv-rconc
[@2: The cat visits the squirrel.[CWA. Example of deepest failure = (rule8 <- rule4 <- FAIL)]]
("cat" "visits" "squirrel" "-")
The mouse eats the dog.
Unknown
rconc
[@1: The mouse eats the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "eats" "dog" "+")
The mouse does not visit the mouse.
Unknown
inv-rconc
[@1: The mouse visits the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "visits" "mouse" "-")
The mouse is young.
Unknown
random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "+")
The cat does not see the mouse.
Unknown
inv-random
[@0: The cat sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "mouse" "-")
The squirrel sees the cat.
Unknown
random
[@0: The squirrel sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "cat" "+")
@0: The cat sees the dog.[(triple1 OR ((triple2) -> rule5))] The dog visits the cat.[(triple2)] The mouse visits the dog.[(triple3)] The squirrel eats the dog.[(triple4)] @1: The dog visits the squirrel.[(((triple3) -> rule7))] The squirrel visits the squirrel.[(((triple4) -> rule8))] @2: The squirrel is cold.[(((((triple3) -> rule7)) -> rule3) OR ((((triple4) -> rule8)) -> rule3))]
The cat sees the dog.
("cat" "sees" "dog" "+")
triple1
((triple2) -> (rule5 % int1))
The cat sees the dog.
("cat" "sees" "dog" "+")
int1
The dog visits the cat.
("dog" "visits" "cat" "+")
triple2
The mouse visits the dog.
("mouse" "visits" "dog" "+")
triple3
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
triple4
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
((triple3) -> (rule7 % int1))
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
((triple4) -> (rule8 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
((((triple3) -> (rule7 % int2))) -> (rule3 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int2
((((triple4) -> (rule8 % int2))) -> (rule3 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int2