The cat needs the dog. The cat sees the dog. The dog chases the mouse. The dog sees the cat. The dog sees the mouse. The mouse chases the cat. The mouse chases the dog. The mouse is kind. The mouse is nice. The mouse needs the cat. The mouse needs the dog. The mouse sees the cat. If someone is kind and they see the mouse then they are blue. If the dog chases the cat then the cat needs the dog. If someone needs the cat then they see the cat. If someone sees the cat and they see the dog then the dog needs the mouse. If someone needs the mouse then the mouse sees the cat. If the dog sees the mouse then the mouse sees the dog. If someone sees the dog then they see the mouse. If someone chases the dog then they need the dog.
The cat needs the dog.
("cat" "needs" "dog" "+")
The cat sees the dog.
("cat" "sees" "dog" "+")
The dog chases the mouse.
("dog" "chases" "mouse" "+")
The dog sees the cat.
("dog" "sees" "cat" "+")
The dog sees the mouse.
("dog" "sees" "mouse" "+")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
The mouse chases the dog.
("mouse" "chases" "dog" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse needs the cat.
("mouse" "needs" "cat" "+")
The mouse needs the dog.
("mouse" "needs" "dog" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
If someone is kind and they see the mouse then they are blue.
((("someone" "is" "kind" "+") ("someone" "sees" "mouse" "+")) -> ("someone" "is" "blue" "+"))
If the dog chases the cat then the cat needs the dog.
((("dog" "chases" "cat" "+")) -> ("cat" "needs" "dog" "+"))
If someone needs the cat then they see the cat.
((("someone" "needs" "cat" "+")) -> ("someone" "sees" "cat" "+"))
If someone sees the cat and they see the dog then the dog needs the mouse.
((("someone" "sees" "cat" "+") ("someone" "sees" "dog" "+")) -> ("dog" "needs" "mouse" "+"))
If someone needs the mouse then the mouse sees the cat.
((("someone" "needs" "mouse" "+")) -> ("mouse" "sees" "cat" "+"))
If the dog sees the mouse then the mouse sees the dog.
((("dog" "sees" "mouse" "+")) -> ("mouse" "sees" "dog" "+"))
If someone sees the dog then they see the mouse.
((("someone" "sees" "dog" "+")) -> ("someone" "sees" "mouse" "+"))
If someone chases the dog then they need the dog.
((("someone" "chases" "dog" "+")) -> ("someone" "needs" "dog" "+"))
The cat needs the dog.
True
1
proof
[(triple1)]
("cat" "needs" "dog" "+")
triple1
The dog does not see the cat.
False
1
inv-proof
[(triple4)]
("dog" "sees" "cat" "-")
triple4
The cat sees the mouse.
True
2
proof
[(((triple2) -> rule7))]
("cat" "sees" "mouse" "+")
((triple2) -> (rule7 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The cat does not see the mouse.
False
2
inv-proof
[(((triple2) -> rule7))]
("cat" "sees" "mouse" "-")
((triple2) -> (rule7 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The mouse sees the mouse.
True
3
proof
[(((((triple5) -> rule6)) -> rule7))]
("mouse" "sees" "mouse" "+")
((((triple5) -> (rule6 % int2))) -> (rule7 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int2
The dog does not need the mouse.
False
4
inv-proof
[(((triple12 ((triple5) -> rule6)) -> rule4) OR ((((triple10) -> rule3) ((triple5) -> rule6)) -> rule4))]
("dog" "needs" "mouse" "-")
((triple12 ((triple5) -> (rule6 % int2))) -> (rule4 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int2
((((triple10) -> (rule3 % int3)) ((triple5) -> (rule6 % int2))) -> (rule4 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int2
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int3
The mouse is blue.
True
5
proof
[(((triple8 ((((triple5) -> rule6)) -> rule7)) -> rule1))]
("mouse" "is" "blue" "+")
((triple8 ((((triple5) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int3
The mouse is not blue.
False
5
inv-proof
[(((triple8 ((((triple5) -> rule6)) -> rule7)) -> rule1))]
("mouse" "is" "blue" "-")
((triple8 ((((triple5) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
The mouse sees the dog.
("mouse" "sees" "dog" "+")
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 dog is blue.
Unknown
rconc
[@1: The dog is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "is" "blue" "+")
The dog does not need the dog.
Unknown
inv-rconc
[@1: The dog needs the dog.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("dog" "needs" "dog" "-")
The cat sees the cat.
Unknown
rconc
[@1: The cat sees the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "sees" "cat" "+")
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 dog is nice.
Unknown
random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "+")
The mouse is not red.
Unknown
inv-random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "-")
The cat chases the dog.
Unknown
random
[@0: The cat chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "dog" "+")
@0: The cat needs the dog.[(triple1)] The cat sees the dog.[(triple2)] The dog chases the mouse.[(triple3)] The dog sees the cat.[(triple4)] The dog sees the mouse.[(triple5)] The mouse chases the cat.[(triple6)] The mouse chases the dog.[(triple7)] The mouse is kind.[(triple8)] The mouse is nice.[(triple9)] The mouse needs the cat.[(triple10)] The mouse needs the dog.[(triple11 OR ((triple7) -> rule8))] The mouse sees the cat.[(triple12 OR ((triple10) -> rule3))] @1: The cat sees the mouse.[(((triple2) -> rule7))] The mouse sees the dog.[(((triple5) -> rule6))] @2: The dog needs the mouse.[(((triple12 ((triple5) -> rule6)) -> rule4) OR ((((triple10) -> rule3) ((triple5) -> rule6)) -> rule4))] The mouse sees the mouse.[(((((triple5) -> rule6)) -> rule7))] @3: The mouse is blue.[(((triple8 ((((triple5) -> rule6)) -> rule7)) -> rule1))]
The cat needs the dog.
("cat" "needs" "dog" "+")
triple1
The cat sees the dog.
("cat" "sees" "dog" "+")
triple2
The dog chases the mouse.
("dog" "chases" "mouse" "+")
triple3
The dog sees the cat.
("dog" "sees" "cat" "+")
triple4
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple5
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple6
The mouse chases the dog.
("mouse" "chases" "dog" "+")
triple7
The mouse is kind.
("mouse" "is" "kind" "+")
triple8
The mouse is nice.
("mouse" "is" "nice" "+")
triple9
The mouse needs the cat.
("mouse" "needs" "cat" "+")
triple10
The mouse needs the dog.
("mouse" "needs" "dog" "+")
triple11
((triple7) -> (rule8 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple12
((triple10) -> (rule3 % int1))
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int1
The cat sees the mouse.
("cat" "sees" "mouse" "+")
((triple2) -> (rule7 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The mouse sees the dog.
("mouse" "sees" "dog" "+")
((triple5) -> (rule6 % int1))
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
((triple12 ((triple5) -> (rule6 % int2))) -> (rule4 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int2
((((triple10) -> (rule3 % int3)) ((triple5) -> (rule6 % int2))) -> (rule4 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int2
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int3
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
((((triple5) -> (rule6 % int2))) -> (rule7 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
((triple8 ((((triple5) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int3