The dog chases the mouse. The dog is round. The dog needs the mouse. The dog sees the mouse. The mouse chases the dog. The mouse is green. The mouse is red. The mouse is rough. The mouse is round. The mouse is young. The mouse needs the dog. The mouse sees the dog. If something is green then it chases the mouse.
The dog chases the mouse.
("dog" "chases" "mouse" "+")
The dog is round.
("dog" "is" "round" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The dog sees the mouse.
("dog" "sees" "mouse" "+")
The mouse chases the dog.
("mouse" "chases" "dog" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse needs the dog.
("mouse" "needs" "dog" "+")
The mouse sees the dog.
("mouse" "sees" "dog" "+")
If something is green then it chases the mouse.
((("something" "is" "green" "+")) -> ("something" "chases" "mouse" "+"))
The mouse chases the dog.
True
1
proof
[(triple5)]
("mouse" "chases" "dog" "+")
triple5
The mouse is not green.
False
1
inv-proof
[(triple6)]
("mouse" "is" "green" "-")
triple6
The mouse chases the mouse.
True
2
proof
[(((triple6) -> rule1))]
("mouse" "chases" "mouse" "+")
((triple6) -> (rule1 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse does not chase the mouse.
False
2
inv-proof
[(((triple6) -> rule1))]
("mouse" "chases" "mouse" "-")
((triple6) -> (rule1 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
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 dog is red.
Unknown
random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "+")
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 sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
@0: The dog chases the mouse.[(triple1)] The dog is round.[(triple2)] The dog needs the mouse.[(triple3)] The dog sees the mouse.[(triple4)] The mouse chases the dog.[(triple5)] The mouse is green.[(triple6)] The mouse is red.[(triple7)] The mouse is rough.[(triple8)] The mouse is round.[(triple9)] The mouse is young.[(triple10)] The mouse needs the dog.[(triple11)] The mouse sees the dog.[(triple12)] @1: The mouse chases the mouse.[(((triple6) -> rule1))]
The dog chases the mouse.
("dog" "chases" "mouse" "+")
triple1
The dog is round.
("dog" "is" "round" "+")
triple2
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple3
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple4
The mouse chases the dog.
("mouse" "chases" "dog" "+")
triple5
The mouse is green.
("mouse" "is" "green" "+")
triple6
The mouse is red.
("mouse" "is" "red" "+")
triple7
The mouse is rough.
("mouse" "is" "rough" "+")
triple8
The mouse is round.
("mouse" "is" "round" "+")
triple9
The mouse is young.
("mouse" "is" "young" "+")
triple10
The mouse needs the dog.
("mouse" "needs" "dog" "+")
triple11
The mouse sees the dog.
("mouse" "sees" "dog" "+")
triple12
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((triple6) -> (rule1 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1