The cat chases the squirrel. The cat needs the squirrel. The dog chases the mouse. The dog visits the squirrel. The mouse chases the cat. The mouse chases the squirrel. The mouse visits the dog. The squirrel chases the dog. The squirrel chases the mouse. The squirrel is blue. The squirrel is kind. The squirrel visits the mouse. If someone needs the cat then the cat chases the dog. If the dog needs the cat and the dog visits the cat then the cat visits the squirrel. If someone chases the squirrel and the squirrel visits the dog then the dog chases the squirrel. If someone is kind then they need the mouse. If someone needs the mouse then the mouse needs the cat. If the mouse chases the squirrel then the squirrel chases the cat.
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
The dog chases the mouse.
("dog" "chases" "mouse" "+")
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
The mouse visits the dog.
("mouse" "visits" "dog" "+")
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
If someone needs the cat then the cat chases the dog.
((("someone" "needs" "cat" "+")) -> ("cat" "chases" "dog" "+"))
If the dog needs the cat and the dog visits the cat then the cat visits the squirrel.
((("dog" "needs" "cat" "+") ("dog" "visits" "cat" "+")) -> ("cat" "visits" "squirrel" "+"))
If someone chases the squirrel and the squirrel visits the dog then the dog chases the squirrel.
((("someone" "chases" "squirrel" "+") ("squirrel" "visits" "dog" "+")) -> ("dog" "chases" "squirrel" "+"))
If someone is kind then they need the mouse.
((("someone" "is" "kind" "+")) -> ("someone" "needs" "mouse" "+"))
If someone needs the mouse then the mouse needs the cat.
((("someone" "needs" "mouse" "+")) -> ("mouse" "needs" "cat" "+"))
If the mouse chases the squirrel then the squirrel chases the cat.
((("mouse" "chases" "squirrel" "+")) -> ("squirrel" "chases" "cat" "+"))
The dog chases the mouse.
True
1
proof
[(triple3)]
("dog" "chases" "mouse" "+")
triple3
The squirrel does not visit the mouse.
False
1
inv-proof
[(triple12)]
("squirrel" "visits" "mouse" "-")
triple12
The squirrel needs the mouse.
True
2
proof
[(((triple11) -> rule4))]
("squirrel" "needs" "mouse" "+")
((triple11) -> (rule4 % int1))
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int1
The squirrel does not need the mouse.
False
2
inv-proof
[(((triple11) -> rule4))]
("squirrel" "needs" "mouse" "-")
((triple11) -> (rule4 % int1))
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int1
The mouse needs the cat.
True
3
proof
[(((((triple11) -> rule4)) -> rule5))]
("mouse" "needs" "cat" "+")
((((triple11) -> (rule4 % int2))) -> (rule5 % int1))
The mouse needs the cat.
("mouse" "needs" "cat" "+")
int1
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int2
The mouse does not need the cat.
False
3
inv-proof
[(((((triple11) -> rule4)) -> rule5))]
("mouse" "needs" "cat" "-")
((((triple11) -> (rule4 % int2))) -> (rule5 % int1))
The mouse needs the cat.
("mouse" "needs" "cat" "+")
int1
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int2
The cat chases the dog.
True
4
proof
[(((((((triple11) -> rule4)) -> rule5)) -> rule1))]
("cat" "chases" "dog" "+")
((((((triple11) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The cat chases the dog.
("cat" "chases" "dog" "+")
int1
The mouse needs the cat.
("mouse" "needs" "cat" "+")
int2
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int3
The cat does not chase the dog.
False
4
inv-proof
[(((((((triple11) -> rule4)) -> rule5)) -> rule1))]
("cat" "chases" "dog" "-")
((((((triple11) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The cat chases the dog.
("cat" "chases" "dog" "+")
int1
The mouse needs the cat.
("mouse" "needs" "cat" "+")
int2
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int3
The mouse does not need the mouse.
Unknown
inv-rconc
[@1: The mouse needs the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "needs" "mouse" "-")
The cat visits the squirrel.
Unknown
rconc
[@1: The cat visits the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "visits" "squirrel" "+")
The cat does not need the mouse.
Unknown
inv-rconc
[@1: The cat needs the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "needs" "mouse" "-")
The dog chases the squirrel.
Unknown
rconc
[@1: The dog chases the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "chases" "squirrel" "+")
The cat is not kind.
Unknown
inv-random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "-")
The mouse is blue.
Unknown
random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "+")
The cat does not chase the cat.
Unknown
inv-random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "-")
The squirrel is green.
Unknown
random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "+")
@0: The cat chases the squirrel.[(triple1)] The cat needs the squirrel.[(triple2)] The dog chases the mouse.[(triple3)] The dog visits the squirrel.[(triple4)] The mouse chases the cat.[(triple5)] The mouse chases the squirrel.[(triple6)] The mouse visits the dog.[(triple7)] The squirrel chases the dog.[(triple8)] The squirrel chases the mouse.[(triple9)] The squirrel is blue.[(triple10)] The squirrel is kind.[(triple11)] The squirrel visits the mouse.[(triple12)] @1: The squirrel chases the cat.[(((triple6) -> rule6))] The squirrel needs the mouse.[(((triple11) -> rule4))] @2: The mouse needs the cat.[(((((triple11) -> rule4)) -> rule5))] @3: The cat chases the dog.[(((((((triple11) -> rule4)) -> rule5)) -> rule1))]
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
triple1
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
triple2
The dog chases the mouse.
("dog" "chases" "mouse" "+")
triple3
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
triple4
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple5
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
triple6
The mouse visits the dog.
("mouse" "visits" "dog" "+")
triple7
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
triple8
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
triple9
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple10
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple11
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
triple12
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
((triple6) -> (rule6 % int1))
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int1
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
((triple11) -> (rule4 % int1))
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int1
The mouse needs the cat.
("mouse" "needs" "cat" "+")
((((triple11) -> (rule4 % int2))) -> (rule5 % int1))
The mouse needs the cat.
("mouse" "needs" "cat" "+")
int1
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int2
The cat chases the dog.
("cat" "chases" "dog" "+")
((((((triple11) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The cat chases the dog.
("cat" "chases" "dog" "+")
int1
The mouse needs the cat.
("mouse" "needs" "cat" "+")
int2
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int3