The dog chases the mouse. The dog is big. The dog is cold. The dog is green. The dog is kind. The dog likes the mouse. The dog needs the mouse. The mouse chases the dog. The mouse is cold. The mouse is kind. The mouse likes the dog. The mouse needs the dog. If someone is green then they need the mouse. If someone needs the dog then the dog chases the mouse. If someone chases the dog then they are green.
The dog chases the mouse.
("dog" "chases" "mouse" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is kind.
("dog" "is" "kind" "+")
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 cold.
("mouse" "is" "cold" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse likes the dog.
("mouse" "likes" "dog" "+")
The mouse needs the dog.
("mouse" "needs" "dog" "+")
If someone is green then they need the mouse.
((("someone" "is" "green" "+")) -> ("someone" "needs" "mouse" "+"))
If someone needs the dog then the dog chases the mouse.
((("someone" "needs" "dog" "+")) -> ("dog" "chases" "mouse" "+"))
If someone chases the dog then they are green.
((("someone" "chases" "dog" "+")) -> ("someone" "is" "green" "+"))
The mouse needs the dog.
True
1
proof
[(triple12)]
("mouse" "needs" "dog" "+")
triple12
The dog is not cold.
False
1
inv-proof
[(triple3)]
("dog" "is" "cold" "-")
triple3
The mouse is green.
True
2
proof
[(((triple8) -> rule3))]
("mouse" "is" "green" "+")
((triple8) -> (rule3 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is not green.
False
2
inv-proof
[(((triple8) -> rule3))]
("mouse" "is" "green" "-")
((triple8) -> (rule3 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse needs the mouse.
True
3
proof
[(((((triple8) -> rule3)) -> rule1))]
("mouse" "needs" "mouse" "+")
((((triple8) -> (rule3 % int2))) -> (rule1 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The mouse does not need the mouse.
False
3
inv-proof
[(((((triple8) -> rule3)) -> rule1))]
("mouse" "needs" "mouse" "-")
((((triple8) -> (rule3 % int2))) -> (rule1 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
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 red.
Unknown
inv-random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
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 likes the dog.
Unknown
random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "+")
@0: The dog chases the mouse.[(triple1 OR ((triple12) -> rule2))] The dog is big.[(triple2)] The dog is cold.[(triple3)] The dog is green.[(triple4)] The dog is kind.[(triple5)] The dog likes the mouse.[(triple6)] The dog needs the mouse.[(triple7 OR ((triple4) -> rule1))] The mouse chases the dog.[(triple8)] The mouse is cold.[(triple9)] The mouse is kind.[(triple10)] The mouse likes the dog.[(triple11)] The mouse needs the dog.[(triple12)] @1: The mouse is green.[(((triple8) -> rule3))] @2: The mouse needs the mouse.[(((((triple8) -> rule3)) -> rule1))]
The dog chases the mouse.
("dog" "chases" "mouse" "+")
triple1
((triple12) -> (rule2 % int1))
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int1
The dog is big.
("dog" "is" "big" "+")
triple2
The dog is cold.
("dog" "is" "cold" "+")
triple3
The dog is green.
("dog" "is" "green" "+")
triple4
The dog is kind.
("dog" "is" "kind" "+")
triple5
The dog likes the mouse.
("dog" "likes" "mouse" "+")
triple6
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple7
((triple4) -> (rule1 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The mouse chases the dog.
("mouse" "chases" "dog" "+")
triple8
The mouse is cold.
("mouse" "is" "cold" "+")
triple9
The mouse is kind.
("mouse" "is" "kind" "+")
triple10
The mouse likes the dog.
("mouse" "likes" "dog" "+")
triple11
The mouse needs the dog.
("mouse" "needs" "dog" "+")
triple12
The mouse is green.
("mouse" "is" "green" "+")
((triple8) -> (rule3 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((((triple8) -> (rule3 % int2))) -> (rule1 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2