The dog eats the mouse. The dog is big. The dog is blue. The dog is green. The dog is round. The dog likes the mouse. The dog needs the mouse. The mouse eats the dog. The mouse likes the dog. The mouse needs the dog. If something eats the mouse and it needs the dog then the mouse likes the dog. If something likes the dog then the dog likes the mouse. If something likes the dog and it is round then the dog is green. If something is round and it needs the mouse then it eats the dog. If something eats the dog then it likes the dog. If something likes the mouse and it needs the mouse then the mouse is not round.
The dog eats the mouse.
("dog" "eats" "mouse" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is round.
("dog" "is" "round" "+")
The dog likes the mouse.
("dog" "likes" "mouse" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The mouse eats the dog.
("mouse" "eats" "dog" "+")
The mouse likes the dog.
("mouse" "likes" "dog" "+")
The mouse needs the dog.
("mouse" "needs" "dog" "+")
If something eats the mouse and it needs the dog then the mouse likes the dog.
((("something" "eats" "mouse" "+") ("something" "needs" "dog" "+")) -> ("mouse" "likes" "dog" "+"))
If something likes the dog then the dog likes the mouse.
((("something" "likes" "dog" "+")) -> ("dog" "likes" "mouse" "+"))
If something likes the dog and it is round then the dog is green.
((("something" "likes" "dog" "+") ("something" "is" "round" "+")) -> ("dog" "is" "green" "+"))
If something is round and it needs the mouse then it eats the dog.
((("something" "is" "round" "+") ("something" "needs" "mouse" "+")) -> ("something" "eats" "dog" "+"))
If something eats the dog then it likes the dog.
((("something" "eats" "dog" "+")) -> ("something" "likes" "dog" "+"))
If something likes the mouse and it needs the mouse then the mouse is not round.
((("something" "likes" "mouse" "+") ("something" "needs" "mouse" "+")) -> ("mouse" "is" "round" "-"))
The dog likes the mouse.
True
1
proof
[(triple6 OR ((triple9) -> rule2) OR ((((triple8) -> rule5)) -> rule2) OR ((((((triple5 triple7) -> rule4)) -> rule5)) -> rule2))]
("dog" "likes" "mouse" "+")
triple6
((triple9) -> (rule2 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
((((triple8) -> (rule5 % int2))) -> (rule2 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int2
((((((triple5 triple7) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
The dog likes the dog.
("dog" "likes" "dog" "+")
int2
The dog eats the dog.
("dog" "eats" "dog" "+")
int3
The dog is not green.
False
1
inv-proof
[(triple4 OR ((((((triple5 triple7) -> rule4)) -> rule5) triple5) -> rule3))]
("dog" "is" "green" "-")
triple4
((((((triple5 triple7) -> (rule4 % int3))) -> (rule5 % int2)) triple5) -> (rule3 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog likes the dog.
("dog" "likes" "dog" "+")
int2
The dog eats the dog.
("dog" "eats" "dog" "+")
int3
The mouse is not round.
True
3
proof
[(((triple6 triple7) -> rule6) OR ((((triple9) -> rule2) triple7) -> rule6) OR ((((((triple8) -> rule5)) -> rule2) triple7) -> rule6) OR ((((((((triple5 triple7) -> rule4)) -> rule5)) -> rule2) triple7) -> rule6))]
("mouse" "is" "round" "-")
((triple6 triple7) -> (rule6 % int1))
The mouse is not round.
("mouse" "is" "round" "-")
int1
((((triple9) -> (rule2 % int2)) triple7) -> (rule6 % int1))
The mouse is not round.
("mouse" "is" "round" "-")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int2
((((((triple8) -> (rule5 % int3))) -> (rule2 % int2)) triple7) -> (rule6 % int1))
The mouse is not round.
("mouse" "is" "round" "-")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int2
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int3
((((((((triple5 triple7) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule2 % int2)) triple7) -> (rule6 % int1))
The mouse is not round.
("mouse" "is" "round" "-")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int2
The dog likes the dog.
("dog" "likes" "dog" "+")
int3
The dog eats the dog.
("dog" "eats" "dog" "+")
int4
The mouse is round.
False
3
inv-proof
[(((triple6 triple7) -> rule6) OR ((((triple9) -> rule2) triple7) -> rule6) OR ((((((triple8) -> rule5)) -> rule2) triple7) -> rule6) OR ((((((((triple5 triple7) -> rule4)) -> rule5)) -> rule2) triple7) -> rule6))]
("mouse" "is" "round" "+")
((triple6 triple7) -> (rule6 % int1))
The mouse is not round.
("mouse" "is" "round" "-")
int1
((((triple9) -> (rule2 % int2)) triple7) -> (rule6 % int1))
The mouse is not round.
("mouse" "is" "round" "-")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int2
((((((triple8) -> (rule5 % int3))) -> (rule2 % int2)) triple7) -> (rule6 % int1))
The mouse is not round.
("mouse" "is" "round" "-")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int2
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int3
((((((((triple5 triple7) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule2 % int2)) triple7) -> (rule6 % int1))
The mouse is not round.
("mouse" "is" "round" "-")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int2
The dog likes the dog.
("dog" "likes" "dog" "+")
int3
The dog eats the dog.
("dog" "eats" "dog" "+")
int4
The dog likes the dog.
True
4
proof
[(((((triple5 triple7) -> rule4)) -> rule5))]
("dog" "likes" "dog" "+")
((((triple5 triple7) -> (rule4 % int2))) -> (rule5 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The dog eats the dog.
("dog" "eats" "dog" "+")
int2
The dog does not like the dog.
False
4
inv-proof
[(((((triple5 triple7) -> rule4)) -> rule5))]
("dog" "likes" "dog" "-")
((((triple5 triple7) -> (rule4 % int2))) -> (rule5 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The dog eats the dog.
("dog" "eats" "dog" "+")
int2
The mouse is not blue.
Unknown
inv-random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "-")
The mouse is big.
Unknown
random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "+")
The mouse is not rough.
Unknown
inv-random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
The dog is not rough.
Unknown
inv-random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "-")
The mouse is green.
Unknown
random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "+")
@0: The dog eats the mouse.[(triple1)] The dog is big.[(triple2)] The dog is blue.[(triple3)] The dog is green.[(triple4 OR ((((((triple5 triple7) -> rule4)) -> rule5) triple5) -> rule3))] The dog is round.[(triple5)] The dog likes the mouse.[(triple6 OR ((triple9) -> rule2) OR ((((triple8) -> rule5)) -> rule2) OR ((((((triple5 triple7) -> rule4)) -> rule5)) -> rule2))] The dog needs the mouse.[(triple7)] The mouse eats the dog.[(triple8)] The mouse likes the dog.[(triple9 OR ((triple8) -> rule5))] The mouse needs the dog.[(triple10)] @1: The dog eats the dog.[(((triple5 triple7) -> rule4))] The mouse is not round.[(((triple6 triple7) -> rule6) OR ((((triple9) -> rule2) triple7) -> rule6) OR ((((((triple8) -> rule5)) -> rule2) triple7) -> rule6) OR ((((((((triple5 triple7) -> rule4)) -> rule5)) -> rule2) triple7) -> rule6))] @2: The dog likes the dog.[(((((triple5 triple7) -> rule4)) -> rule5))]
The dog eats the mouse.
("dog" "eats" "mouse" "+")
triple1
The dog is big.
("dog" "is" "big" "+")
triple2
The dog is blue.
("dog" "is" "blue" "+")
triple3
The dog is green.
("dog" "is" "green" "+")
triple4
((((((triple5 triple7) -> (rule4 % int3))) -> (rule5 % int2)) triple5) -> (rule3 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog likes the dog.
("dog" "likes" "dog" "+")
int2
The dog eats the dog.
("dog" "eats" "dog" "+")
int3
The dog is round.
("dog" "is" "round" "+")
triple5
The dog likes the mouse.
("dog" "likes" "mouse" "+")
triple6
((triple9) -> (rule2 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
((((triple8) -> (rule5 % int2))) -> (rule2 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int2
((((((triple5 triple7) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
The dog likes the dog.
("dog" "likes" "dog" "+")
int2
The dog eats the dog.
("dog" "eats" "dog" "+")
int3
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple7
The mouse eats the dog.
("mouse" "eats" "dog" "+")
triple8
The mouse likes the dog.
("mouse" "likes" "dog" "+")
triple9
((triple8) -> (rule5 % int1))
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int1
The mouse needs the dog.
("mouse" "needs" "dog" "+")
triple10
The dog eats the dog.
("dog" "eats" "dog" "+")
((triple5 triple7) -> (rule4 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1
The mouse is not round.
("mouse" "is" "round" "-")
((triple6 triple7) -> (rule6 % int1))
The mouse is not round.
("mouse" "is" "round" "-")
int1
((((triple9) -> (rule2 % int2)) triple7) -> (rule6 % int1))
The mouse is not round.
("mouse" "is" "round" "-")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int2
((((((triple8) -> (rule5 % int3))) -> (rule2 % int2)) triple7) -> (rule6 % int1))
The mouse is not round.
("mouse" "is" "round" "-")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int2
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int3
((((((((triple5 triple7) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule2 % int2)) triple7) -> (rule6 % int1))
The mouse is not round.
("mouse" "is" "round" "-")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int2
The dog likes the dog.
("dog" "likes" "dog" "+")
int3
The dog eats the dog.
("dog" "eats" "dog" "+")
int4
The dog likes the dog.
("dog" "likes" "dog" "+")
((((triple5 triple7) -> (rule4 % int2))) -> (rule5 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The dog eats the dog.
("dog" "eats" "dog" "+")
int2