The cat eats the dog. The dog chases the cat. The mouse eats the squirrel. The squirrel is kind. If someone is kind and they chase the mouse then they are cold. If someone eats the cat then they eat the dog. If someone eats the squirrel and the squirrel is blue then the squirrel eats the cat. If someone chases the squirrel then the squirrel sees the dog. If someone is cold then they chase the mouse. If someone is kind then they are blue.
The cat eats the dog.
("cat" "eats" "dog" "+")
The dog chases the cat.
("dog" "chases" "cat" "+")
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
If someone is kind and they chase the mouse then they are cold.
((("someone" "is" "kind" "+") ("someone" "chases" "mouse" "+")) -> ("someone" "is" "cold" "+"))
If someone eats the cat then they eat the dog.
((("someone" "eats" "cat" "+")) -> ("someone" "eats" "dog" "+"))
If someone eats the squirrel and the squirrel is blue then the squirrel eats the cat.
((("someone" "eats" "squirrel" "+") ("squirrel" "is" "blue" "+")) -> ("squirrel" "eats" "cat" "+"))
If someone chases the squirrel then the squirrel sees the dog.
((("someone" "chases" "squirrel" "+")) -> ("squirrel" "sees" "dog" "+"))
If someone is cold then they chase the mouse.
((("someone" "is" "cold" "+")) -> ("someone" "chases" "mouse" "+"))
If someone is kind then they are blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
The squirrel is kind.
True
1
proof
[(triple4)]
("squirrel" "is" "kind" "+")
triple4
The dog does not chase the cat.
False
1
inv-proof
[(triple2)]
("dog" "chases" "cat" "-")
triple2
The squirrel is blue.
True
2
proof
[(((triple4) -> rule6))]
("squirrel" "is" "blue" "+")
((triple4) -> (rule6 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is not blue.
False
2
inv-proof
[(((triple4) -> rule6))]
("squirrel" "is" "blue" "-")
((triple4) -> (rule6 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel eats the cat.
True
4
proof
[(((triple3 ((triple4) -> rule6)) -> rule3))]
("squirrel" "eats" "cat" "+")
((triple3 ((triple4) -> (rule6 % int2))) -> (rule3 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel does not eat the cat.
False
4
inv-proof
[(((triple3 ((triple4) -> rule6)) -> rule3))]
("squirrel" "eats" "cat" "-")
((triple3 ((triple4) -> (rule6 % int2))) -> (rule3 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel eats the dog.
True
5
proof
[(((((triple3 ((triple4) -> rule6)) -> rule3)) -> rule2))]
("squirrel" "eats" "dog" "+")
((((triple3 ((triple4) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
int1
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int2
The squirrel is blue.
("squirrel" "is" "blue" "+")
int3
The squirrel does not eat the dog.
False
5
inv-proof
[(((((triple3 ((triple4) -> rule6)) -> rule3)) -> rule2))]
("squirrel" "eats" "dog" "-")
((((triple3 ((triple4) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
int1
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int2
The squirrel is blue.
("squirrel" "is" "blue" "+")
int3
The dog is not blue.
Unknown
inv-rconc
[@1: The dog is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "is" "blue" "-")
The mouse chases the mouse.
Unknown
rconc
[@2: The mouse chases the mouse.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("mouse" "chases" "mouse" "+")
The mouse is not cold.
Unknown
inv-rconc
[@1: The mouse is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "is" "cold" "-")
The cat chases the mouse.
Unknown
rconc
[@2: The cat chases the mouse.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("cat" "chases" "mouse" "+")
The dog does not chase the dog.
Unknown
inv-random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "-")
The squirrel eats the squirrel.
Unknown
random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "+")
The mouse does not see the dog.
Unknown
inv-random
[@0: The mouse sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "dog" "-")
The cat eats the squirrel.
Unknown
random
[@0: The cat eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "squirrel" "+")
@0: The cat eats the dog.[(triple1)] The dog chases the cat.[(triple2)] The mouse eats the squirrel.[(triple3)] The squirrel is kind.[(triple4)] @1: The squirrel is blue.[(((triple4) -> rule6))] @2: The squirrel eats the cat.[(((triple3 ((triple4) -> rule6)) -> rule3))] @3: The squirrel eats the dog.[(((((triple3 ((triple4) -> rule6)) -> rule3)) -> rule2))]
The cat eats the dog.
("cat" "eats" "dog" "+")
triple1
The dog chases the cat.
("dog" "chases" "cat" "+")
triple2
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
triple3
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple4
The squirrel is blue.
("squirrel" "is" "blue" "+")
((triple4) -> (rule6 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
((triple3 ((triple4) -> (rule6 % int2))) -> (rule3 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
((((triple3 ((triple4) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
int1
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int2
The squirrel is blue.
("squirrel" "is" "blue" "+")
int3