The dog is blue. The dog is cold. The dog is nice. The dog is red. The dog is rough. The dog needs the mouse. The dog sees the mouse. The dog visits the mouse. The mouse is blue. The mouse is cold. The mouse is nice. The mouse is red. The mouse is rough. The mouse needs the dog. The mouse sees the dog. The mouse visits the dog. If something visits the mouse and the mouse is rough then the mouse is cold. If something is nice then it sees the mouse. If the dog is rough then the dog needs the mouse. If the mouse sees the dog and the dog sees the mouse then the mouse needs the dog. If something sees the mouse and the mouse is blue then it needs the mouse. If something needs the dog then it is blue.
The dog is blue.
("dog" "is" "blue" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog is red.
("dog" "is" "red" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The dog sees the mouse.
("dog" "sees" "mouse" "+")
The dog visits the mouse.
("dog" "visits" "mouse" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse needs the dog.
("mouse" "needs" "dog" "+")
The mouse sees the dog.
("mouse" "sees" "dog" "+")
The mouse visits the dog.
("mouse" "visits" "dog" "+")
If something visits the mouse and the mouse is rough then the mouse is cold.
((("something" "visits" "mouse" "+") ("mouse" "is" "rough" "+")) -> ("mouse" "is" "cold" "+"))
If something is nice then it sees the mouse.
((("something" "is" "nice" "+")) -> ("something" "sees" "mouse" "+"))
If the dog is rough then the dog needs the mouse.
((("dog" "is" "rough" "+")) -> ("dog" "needs" "mouse" "+"))
If the mouse sees the dog and the dog sees the mouse then the mouse needs the dog.
((("mouse" "sees" "dog" "+") ("dog" "sees" "mouse" "+")) -> ("mouse" "needs" "dog" "+"))
If something sees the mouse and the mouse is blue then it needs the mouse.
((("something" "sees" "mouse" "+") ("mouse" "is" "blue" "+")) -> ("something" "needs" "mouse" "+"))
If something needs the dog then it is blue.
((("something" "needs" "dog" "+")) -> ("something" "is" "blue" "+"))
The dog is rough.
True
1
proof
[(triple5)]
("dog" "is" "rough" "+")
triple5
The mouse is not nice.
False
1
inv-proof
[(triple11)]
("mouse" "is" "nice" "-")
triple11
The mouse sees the mouse.
True
2
proof
[(((triple11) -> rule2))]
("mouse" "sees" "mouse" "+")
((triple11) -> (rule2 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse does not see the mouse.
False
2
inv-proof
[(((triple11) -> rule2))]
("mouse" "sees" "mouse" "-")
((triple11) -> (rule2 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse needs the mouse.
True
4
proof
[(((((triple11) -> rule2) triple9) -> rule5) OR ((((triple11) -> rule2) ((triple14) -> rule6)) -> rule5) OR ((((triple11) -> rule2) ((((triple15 triple7) -> rule4)) -> rule6)) -> rule5) OR ((((triple11) -> rule2) ((((triple15 ((triple3) -> rule2)) -> rule4)) -> rule6)) -> rule5))]
("mouse" "needs" "mouse" "+")
((((triple11) -> (rule2 % int2)) triple9) -> (rule5 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
((((triple11) -> (rule2 % int3)) ((triple14) -> (rule6 % int2))) -> (rule5 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int3
((((triple11) -> (rule2 % int4)) ((((triple15 triple7) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int3
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int4
((((triple11) -> (rule2 % int5)) ((((triple15 ((triple3) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int3
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int4
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int5
The mouse does not need the mouse.
False
4
inv-proof
[(((((triple11) -> rule2) triple9) -> rule5) OR ((((triple11) -> rule2) ((triple14) -> rule6)) -> rule5) OR ((((triple11) -> rule2) ((((triple15 triple7) -> rule4)) -> rule6)) -> rule5) OR ((((triple11) -> rule2) ((((triple15 ((triple3) -> rule2)) -> rule4)) -> rule6)) -> rule5))]
("mouse" "needs" "mouse" "-")
((((triple11) -> (rule2 % int2)) triple9) -> (rule5 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
((((triple11) -> (rule2 % int3)) ((triple14) -> (rule6 % int2))) -> (rule5 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int3
((((triple11) -> (rule2 % int4)) ((((triple15 triple7) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int3
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int4
((((triple11) -> (rule2 % int5)) ((((triple15 ((triple3) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int3
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int4
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int5
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 dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
The mouse does not visit the mouse.
Unknown
inv-random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "-")
The dog visits the dog.
Unknown
random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "+")
@0: The dog is blue.[(triple1)] The dog is cold.[(triple2)] The dog is nice.[(triple3)] The dog is red.[(triple4)] The dog is rough.[(triple5)] The dog needs the mouse.[(triple6 OR ((triple5) -> rule3) OR ((triple7 triple9) -> rule5) OR ((triple7 ((triple14) -> rule6)) -> rule5) OR ((((triple3) -> rule2) triple9) -> rule5) OR ((((triple3) -> rule2) ((triple14) -> rule6)) -> rule5) OR ((triple7 ((((triple15 triple7) -> rule4)) -> rule6)) -> rule5) OR ((((triple3) -> rule2) ((((triple15 triple7) -> rule4)) -> rule6)) -> rule5) OR ((triple7 ((((triple15 ((triple3) -> rule2)) -> rule4)) -> rule6)) -> rule5) OR ((((triple3) -> rule2) ((((triple15 ((triple3) -> rule2)) -> rule4)) -> rule6)) -> rule5))] The dog sees the mouse.[(triple7 OR ((triple3) -> rule2))] The dog visits the mouse.[(triple8)] The mouse is blue.[(triple9 OR ((triple14) -> rule6) OR ((((triple15 triple7) -> rule4)) -> rule6) OR ((((triple15 ((triple3) -> rule2)) -> rule4)) -> rule6))] The mouse is cold.[(triple10 OR ((triple8 triple13) -> rule1))] The mouse is nice.[(triple11)] The mouse is red.[(triple12)] The mouse is rough.[(triple13)] The mouse needs the dog.[(triple14 OR ((triple15 triple7) -> rule4) OR ((triple15 ((triple3) -> rule2)) -> rule4))] The mouse sees the dog.[(triple15)] The mouse visits the dog.[(triple16)] @1: The mouse sees the mouse.[(((triple11) -> rule2))] @2: The mouse needs the mouse.[(((((triple11) -> rule2) triple9) -> rule5) OR ((((triple11) -> rule2) ((triple14) -> rule6)) -> rule5) OR ((((triple11) -> rule2) ((((triple15 triple7) -> rule4)) -> rule6)) -> rule5) OR ((((triple11) -> rule2) ((((triple15 ((triple3) -> rule2)) -> rule4)) -> rule6)) -> rule5))]
The dog is blue.
("dog" "is" "blue" "+")
triple1
The dog is cold.
("dog" "is" "cold" "+")
triple2
The dog is nice.
("dog" "is" "nice" "+")
triple3
The dog is red.
("dog" "is" "red" "+")
triple4
The dog is rough.
("dog" "is" "rough" "+")
triple5
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple6
((triple5) -> (rule3 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
((triple7 triple9) -> (rule5 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
((triple7 ((triple14) -> (rule6 % int2))) -> (rule5 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
((((triple3) -> (rule2 % int2)) triple9) -> (rule5 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int2
((((triple3) -> (rule2 % int3)) ((triple14) -> (rule6 % int2))) -> (rule5 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int3
((triple7 ((((triple15 triple7) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int3
((((triple3) -> (rule2 % int4)) ((((triple15 triple7) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int3
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int4
((triple7 ((((triple15 ((triple3) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int3
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int4
((((triple3) -> (rule2 % int4)) ((((triple15 ((triple3) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int3
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int4
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple7
((triple3) -> (rule2 % int1))
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int1
The dog visits the mouse.
("dog" "visits" "mouse" "+")
triple8
The mouse is blue.
("mouse" "is" "blue" "+")
triple9
((triple14) -> (rule6 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
((((triple15 triple7) -> (rule4 % int2))) -> (rule6 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int2
((((triple15 ((triple3) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int2
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int3
The mouse is cold.
("mouse" "is" "cold" "+")
triple10
((triple8 triple13) -> (rule1 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
triple11
The mouse is red.
("mouse" "is" "red" "+")
triple12
The mouse is rough.
("mouse" "is" "rough" "+")
triple13
The mouse needs the dog.
("mouse" "needs" "dog" "+")
triple14
((triple15 triple7) -> (rule4 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
((triple15 ((triple3) -> (rule2 % int2))) -> (rule4 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int2
The mouse sees the dog.
("mouse" "sees" "dog" "+")
triple15
The mouse visits the dog.
("mouse" "visits" "dog" "+")
triple16
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
((triple11) -> (rule2 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((((triple11) -> (rule2 % int2)) triple9) -> (rule5 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
((((triple11) -> (rule2 % int3)) ((triple14) -> (rule6 % int2))) -> (rule5 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int3
((((triple11) -> (rule2 % int4)) ((((triple15 triple7) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int3
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int4
((((triple11) -> (rule2 % int5)) ((((triple15 ((triple3) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int3
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int4
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int5