The dog is big. The dog is blue. The dog is cold. The dog is nice. The dog is rough. The dog likes the mouse. The dog needs the mouse. The dog sees the mouse. The mouse is big. The mouse is blue. The mouse is cold. The mouse is nice. The mouse is rough. The mouse likes the dog. The mouse needs the dog. The mouse sees the dog. If someone is blue then they like the mouse. If someone is rough then they need the dog. If someone is blue and big then they need the dog. If someone sees the dog then the dog sees the mouse. If the mouse needs the dog then the mouse likes the dog. If someone is big and they like the mouse then the mouse needs the dog.
The dog is big.
("dog" "is" "big" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog likes the mouse.
("dog" "likes" "mouse" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The dog sees the mouse.
("dog" "sees" "mouse" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse likes the dog.
("mouse" "likes" "dog" "+")
The mouse needs the dog.
("mouse" "needs" "dog" "+")
The mouse sees the dog.
("mouse" "sees" "dog" "+")
If someone is blue then they like the mouse.
((("someone" "is" "blue" "+")) -> ("someone" "likes" "mouse" "+"))
If someone is rough then they need the dog.
((("someone" "is" "rough" "+")) -> ("someone" "needs" "dog" "+"))
If someone is blue and big then they need the dog.
((("someone" "is" "blue" "+") ("someone" "is" "big" "+")) -> ("someone" "needs" "dog" "+"))
If someone sees the dog then the dog sees the mouse.
((("someone" "sees" "dog" "+")) -> ("dog" "sees" "mouse" "+"))
If the mouse needs the dog then the mouse likes the dog.
((("mouse" "needs" "dog" "+")) -> ("mouse" "likes" "dog" "+"))
If someone is big and they like the mouse then the mouse needs the dog.
((("someone" "is" "big" "+") ("someone" "likes" "mouse" "+")) -> ("mouse" "needs" "dog" "+"))
The dog is nice.
True
1
proof
[(triple4)]
("dog" "is" "nice" "+")
triple4
The dog is not big.
False
1
inv-proof
[(triple1)]
("dog" "is" "big" "-")
triple1
The mouse likes the mouse.
True
2
proof
[(((triple10) -> rule1))]
("mouse" "likes" "mouse" "+")
((triple10) -> (rule1 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The dog does not need the dog.
False
2
inv-proof
[(((triple5) -> rule2) OR ((triple2 triple1) -> rule3))]
("dog" "needs" "dog" "-")
((triple5) -> (rule2 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
((triple2 triple1) -> (rule3 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog does not like the dog.
Unknown
inv-random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "-")
The mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
The mouse does not see the mouse.
Unknown
inv-random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "-")
The dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
@0: The dog is big.[(triple1)] The dog is blue.[(triple2)] The dog is cold.[(triple3)] The dog is nice.[(triple4)] The dog is rough.[(triple5)] The dog likes the mouse.[(triple6 OR ((triple2) -> rule1))] The dog needs the mouse.[(triple7)] The dog sees the mouse.[(triple8 OR ((triple16) -> rule4))] The mouse is big.[(triple9)] The mouse is blue.[(triple10)] The mouse is cold.[(triple11)] The mouse is nice.[(triple12)] The mouse is rough.[(triple13)] The mouse likes the dog.[(triple14 OR ((triple15) -> rule5) OR ((((triple13) -> rule2)) -> rule5) OR ((((triple1 triple6) -> rule6)) -> rule5) OR ((((triple10 triple9) -> rule3)) -> rule5) OR ((((triple1 ((triple2) -> rule1)) -> rule6)) -> rule5) OR ((((triple9 ((triple10) -> rule1)) -> rule6)) -> rule5))] The mouse needs the dog.[(triple15 OR ((triple13) -> rule2) OR ((triple1 triple6) -> rule6) OR ((triple10 triple9) -> rule3) OR ((triple1 ((triple2) -> rule1)) -> rule6) OR ((triple9 ((triple10) -> rule1)) -> rule6))] The mouse sees the dog.[(triple16)] @1: The dog needs the dog.[(((triple5) -> rule2) OR ((triple2 triple1) -> rule3))] The mouse likes the mouse.[(((triple10) -> rule1))]
The dog is big.
("dog" "is" "big" "+")
triple1
The dog is blue.
("dog" "is" "blue" "+")
triple2
The dog is cold.
("dog" "is" "cold" "+")
triple3
The dog is nice.
("dog" "is" "nice" "+")
triple4
The dog is rough.
("dog" "is" "rough" "+")
triple5
The dog likes the mouse.
("dog" "likes" "mouse" "+")
triple6
((triple2) -> (rule1 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple7
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple8
((triple16) -> (rule4 % int1))
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
triple9
The mouse is blue.
("mouse" "is" "blue" "+")
triple10
The mouse is cold.
("mouse" "is" "cold" "+")
triple11
The mouse is nice.
("mouse" "is" "nice" "+")
triple12
The mouse is rough.
("mouse" "is" "rough" "+")
triple13
The mouse likes the dog.
("mouse" "likes" "dog" "+")
triple14
((triple15) -> (rule5 % int1))
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int1
((((triple13) -> (rule2 % int2))) -> (rule5 % int1))
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int1
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int2
((((triple1 triple6) -> (rule6 % int2))) -> (rule5 % int1))
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int1
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int2
((((triple10 triple9) -> (rule3 % int2))) -> (rule5 % int1))
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int1
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int2
((((triple1 ((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int1
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int2
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int3
((((triple9 ((triple10) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int1
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int2
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int3
The mouse needs the dog.
("mouse" "needs" "dog" "+")
triple15
((triple13) -> (rule2 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
((triple1 triple6) -> (rule6 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
((triple10 triple9) -> (rule3 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
((triple1 ((triple2) -> (rule1 % int2))) -> (rule6 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int2
((triple9 ((triple10) -> (rule1 % int2))) -> (rule6 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int2
The mouse sees the dog.
("mouse" "sees" "dog" "+")
triple16
The dog needs the dog.
("dog" "needs" "dog" "+")
((triple5) -> (rule2 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
((triple2 triple1) -> (rule3 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
((triple10) -> (rule1 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1