The dog chases the mouse. The dog is blue. The dog is nice. The dog is red. The dog likes the mouse. The dog needs the mouse. The mouse chases the dog. The mouse is blue. The mouse likes the dog. The mouse needs the dog. If the dog chases the mouse and the mouse is blue then the mouse likes the dog. If someone likes the mouse and the mouse is blue then the mouse is nice. If someone is cold then they need the dog. If someone is red then they are cold. All nice people are red. If someone chases the mouse and they are blue then the mouse needs the dog. If someone needs the mouse and they like the dog then the mouse is cold. If someone likes the mouse then they need the dog.
The dog chases the mouse.
("dog" "chases" "mouse" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog is red.
("dog" "is" "red" "+")
The dog likes the mouse.
("dog" "likes" "mouse" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The mouse chases the dog.
("mouse" "chases" "dog" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse likes the dog.
("mouse" "likes" "dog" "+")
The mouse needs the dog.
("mouse" "needs" "dog" "+")
If the dog chases the mouse and the mouse is blue then the mouse likes the dog.
((("dog" "chases" "mouse" "+") ("mouse" "is" "blue" "+")) -> ("mouse" "likes" "dog" "+"))
If someone likes the mouse and the mouse is blue then the mouse is nice.
((("someone" "likes" "mouse" "+") ("mouse" "is" "blue" "+")) -> ("mouse" "is" "nice" "+"))
If someone is cold then they need the dog.
((("someone" "is" "cold" "+")) -> ("someone" "needs" "dog" "+"))
If someone is red then they are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
All nice people are red.
((("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
If someone chases the mouse and they are blue then the mouse needs the dog.
((("someone" "chases" "mouse" "+") ("someone" "is" "blue" "+")) -> ("mouse" "needs" "dog" "+"))
If someone needs the mouse and they like the dog then the mouse is cold.
((("someone" "needs" "mouse" "+") ("someone" "likes" "dog" "+")) -> ("mouse" "is" "cold" "+"))
If someone likes the mouse then they need the dog.
((("someone" "likes" "mouse" "+")) -> ("someone" "needs" "dog" "+"))
The mouse likes the dog.
True
1
proof
[(triple9 OR ((triple1 triple8) -> rule1))]
("mouse" "likes" "dog" "+")
triple9
((triple1 triple8) -> (rule1 % int1))
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int1
The mouse is not blue.
False
1
inv-proof
[(triple8)]
("mouse" "is" "blue" "-")
triple8
The dog is cold.
True
2
proof
[(((triple4) -> rule4) OR ((((triple3) -> rule5)) -> rule4))]
("dog" "is" "cold" "+")
((triple4) -> (rule4 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule4 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog is not cold.
False
2
inv-proof
[(((triple4) -> rule4) OR ((((triple3) -> rule5)) -> rule4))]
("dog" "is" "cold" "-")
((triple4) -> (rule4 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule4 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The mouse is red.
True
4
proof
[(((((triple5 triple8) -> rule2)) -> rule5))]
("mouse" "is" "red" "+")
((((triple5 triple8) -> (rule2 % int2))) -> (rule5 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse is not red.
False
4
inv-proof
[(((((triple5 triple8) -> rule2)) -> rule5))]
("mouse" "is" "red" "-")
((((triple5 triple8) -> (rule2 % int2))) -> (rule5 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse is cold.
True
5
proof
[(((((((triple5 triple8) -> rule2)) -> rule5)) -> rule4))]
("mouse" "is" "cold" "+")
((((((triple5 triple8) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
int3
The mouse is not cold.
False
5
inv-proof
[(((((((triple5 triple8) -> rule2)) -> rule5)) -> rule4))]
("mouse" "is" "cold" "-")
((((((triple5 triple8) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
int3
The mouse does not need the mouse.
Unknown
inv-random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "-")
The mouse is young.
Unknown
random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "+")
The dog does not chase the dog.
Unknown
inv-random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "-")
The mouse chases the mouse.
Unknown
random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "+")
The dog is not young.
Unknown
inv-random
[@0: The dog is young.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "young" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
@0: The dog chases the mouse.[(triple1)] The dog is blue.[(triple2)] The dog is nice.[(triple3)] The dog is red.[(triple4 OR ((triple3) -> rule5))] The dog likes the mouse.[(triple5)] The dog needs the mouse.[(triple6)] The mouse chases the dog.[(triple7)] The mouse is blue.[(triple8)] The mouse likes the dog.[(triple9 OR ((triple1 triple8) -> rule1))] The mouse needs the dog.[(triple10 OR ((triple1 triple2) -> rule6) OR ((((((((triple5 triple8) -> rule2)) -> rule5)) -> rule4)) -> rule3))] @1: The dog is cold.[(((triple4) -> rule4) OR ((((triple3) -> rule5)) -> rule4))] The dog needs the dog.[(((triple5) -> rule8) OR ((((triple4) -> rule4)) -> rule3) OR ((((((triple3) -> rule5)) -> rule4)) -> rule3))] The mouse is nice.[(((triple5 triple8) -> rule2))] @2: The mouse is red.[(((((triple5 triple8) -> rule2)) -> rule5))] @3: The mouse is cold.[(((((((triple5 triple8) -> rule2)) -> rule5)) -> rule4))]
The dog chases the mouse.
("dog" "chases" "mouse" "+")
triple1
The dog is blue.
("dog" "is" "blue" "+")
triple2
The dog is nice.
("dog" "is" "nice" "+")
triple3
The dog is red.
("dog" "is" "red" "+")
triple4
((triple3) -> (rule5 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
triple5
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple6
The mouse chases the dog.
("mouse" "chases" "dog" "+")
triple7
The mouse is blue.
("mouse" "is" "blue" "+")
triple8
The mouse likes the dog.
("mouse" "likes" "dog" "+")
triple9
((triple1 triple8) -> (rule1 % int1))
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int1
The mouse needs the dog.
("mouse" "needs" "dog" "+")
triple10
((triple1 triple2) -> (rule6 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
((((((((triple5 triple8) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse is red.
("mouse" "is" "red" "+")
int3
The mouse is nice.
("mouse" "is" "nice" "+")
int4
The dog is cold.
("dog" "is" "cold" "+")
((triple4) -> (rule4 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule4 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog needs the dog.
("dog" "needs" "dog" "+")
((triple5) -> (rule8 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
((((triple4) -> (rule4 % int2))) -> (rule3 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
int2
((((((triple3) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
int2
The dog is red.
("dog" "is" "red" "+")
int3
The mouse is nice.
("mouse" "is" "nice" "+")
((triple5 triple8) -> (rule2 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
((((triple5 triple8) -> (rule2 % int2))) -> (rule5 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
((((((triple5 triple8) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
int3