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