The dog likes the mouse. The mouse needs the dog. If something sees the mouse then it sees the dog. If something is nice then it sees the mouse. If something needs the dog then the dog needs the mouse. If something likes the mouse then the mouse needs the dog. If something likes the dog and it needs the dog then the dog is blue. If the dog needs the mouse then the dog sees the mouse.
The dog likes the mouse.
("dog" "likes" "mouse" "+")
The mouse needs the dog.
("mouse" "needs" "dog" "+")
If something sees the mouse then it sees the dog.
((("something" "sees" "mouse" "+")) -> ("something" "sees" "dog" "+"))
If something is nice then it sees the mouse.
((("something" "is" "nice" "+")) -> ("something" "sees" "mouse" "+"))
If something needs the dog then the dog needs the mouse.
((("something" "needs" "dog" "+")) -> ("dog" "needs" "mouse" "+"))
If something likes the mouse then the mouse needs the dog.
((("something" "likes" "mouse" "+")) -> ("mouse" "needs" "dog" "+"))
If something likes the dog and it needs the dog then the dog is blue.
((("something" "likes" "dog" "+") ("something" "needs" "dog" "+")) -> ("dog" "is" "blue" "+"))
If the dog needs the mouse then the dog sees the mouse.
((("dog" "needs" "mouse" "+")) -> ("dog" "sees" "mouse" "+"))
The dog likes the mouse.
True
1
proof
[(triple1)]
("dog" "likes" "mouse" "+")
triple1
The dog does not like the mouse.
False
1
inv-proof
[(triple1)]
("dog" "likes" "mouse" "-")
triple1
The dog needs the mouse.
True
2
proof
[(((triple2) -> rule3) OR ((((triple1) -> rule4)) -> rule3))]
("dog" "needs" "mouse" "+")
((triple2) -> (rule3 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int2
The dog does not need the mouse.
False
2
inv-proof
[(((triple2) -> rule3) OR ((((triple1) -> rule4)) -> rule3))]
("dog" "needs" "mouse" "-")
((triple2) -> (rule3 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int2
The dog sees the mouse.
True
3
proof
[(((((triple2) -> rule3)) -> rule6) OR ((((((triple1) -> rule4)) -> rule3)) -> rule6))]
("dog" "sees" "mouse" "+")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int2
((((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int2
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int3
The dog does not see the mouse.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule6) OR ((((((triple1) -> rule4)) -> rule3)) -> rule6))]
("dog" "sees" "mouse" "-")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int2
((((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int2
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int3
The dog sees the dog.
True
4
proof
[(((((((triple2) -> rule3)) -> rule6)) -> rule1) OR ((((((((triple1) -> rule4)) -> rule3)) -> rule6)) -> rule1))]
("dog" "sees" "dog" "+")
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int2
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int3
((((((((triple1) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int2
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int3
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int4
The dog does not see the dog.
False
4
inv-proof
[(((((((triple2) -> rule3)) -> rule6)) -> rule1) OR ((((((((triple1) -> rule4)) -> rule3)) -> rule6)) -> rule1))]
("dog" "sees" "dog" "-")
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int2
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int3
((((((((triple1) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int2
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int3
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int4
The mouse does not see the dog.
Unknown
inv-rconc
[@2: The mouse sees the dog.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("mouse" "sees" "dog" "-")
The mouse sees the mouse.
Unknown
rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "sees" "mouse" "+")
The dog is not blue.
Unknown
inv-rconc
[@1: The dog is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "is" "blue" "-")
The dog is nice.
Unknown
random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "+")
The dog does not need the dog.
Unknown
inv-random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "-")
The mouse is blue.
Unknown
random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "+")
The mouse is not green.
Unknown
inv-random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "-")
The mouse is young.
Unknown
random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "+")
@0: The dog likes the mouse.[(triple1)] The mouse needs the dog.[(triple2 OR ((triple1) -> rule4))] @1: The dog needs the mouse.[(((triple2) -> rule3) OR ((((triple1) -> rule4)) -> rule3))] @2: The dog sees the mouse.[(((((triple2) -> rule3)) -> rule6) OR ((((((triple1) -> rule4)) -> rule3)) -> rule6))] @3: The dog sees the dog.[(((((((triple2) -> rule3)) -> rule6)) -> rule1) OR ((((((((triple1) -> rule4)) -> rule3)) -> rule6)) -> rule1))]
The dog likes the mouse.
("dog" "likes" "mouse" "+")
triple1
The mouse needs the dog.
("mouse" "needs" "dog" "+")
triple2
((triple1) -> (rule4 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
((triple2) -> (rule3 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int2
The dog sees the mouse.
("dog" "sees" "mouse" "+")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int2
((((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int2
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int3
The dog sees the dog.
("dog" "sees" "dog" "+")
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int2
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int3
((((((((triple1) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int2
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int3
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int4