The cat chases the mouse. The cat chases the tiger. The cat is green. The cat needs the tiger. The cat sees the mouse. The cat sees the tiger. The mouse chases the cat. The mouse needs the tiger. The mouse sees the cat. The mouse sees the tiger. The tiger chases the cat. The tiger is green. The tiger needs the mouse. The tiger sees the cat. The tiger sees the mouse. If someone needs the cat then the cat chases the mouse. If someone chases the tiger then the tiger is young.
The cat chases the mouse.
("cat" "chases" "mouse" "+")
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The cat is green.
("cat" "is" "green" "+")
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The cat sees the mouse.
("cat" "sees" "mouse" "+")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The tiger chases the cat.
("tiger" "chases" "cat" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
If someone needs the cat then the cat chases the mouse.
((("someone" "needs" "cat" "+")) -> ("cat" "chases" "mouse" "+"))
If someone chases the tiger then the tiger is young.
((("someone" "chases" "tiger" "+")) -> ("tiger" "is" "young" "+"))
The mouse needs the tiger.
True
1
proof
[(triple8)]
("mouse" "needs" "tiger" "+")
triple8
The cat is not green.
False
1
inv-proof
[(triple3)]
("cat" "is" "green" "-")
triple3
The tiger is young.
True
2
proof
[(((triple2) -> rule2))]
("tiger" "is" "young" "+")
((triple2) -> (rule2 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is not young.
False
2
inv-proof
[(((triple2) -> rule2))]
("tiger" "is" "young" "-")
((triple2) -> (rule2 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
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 chases the mouse.
Unknown
random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "+")
The cat does not need the mouse.
Unknown
inv-random
[@0: The cat needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "mouse" "-")
The mouse is kind.
Unknown
random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "+")
@0: The cat chases the mouse.[(triple1)] The cat chases the tiger.[(triple2)] The cat is green.[(triple3)] The cat needs the tiger.[(triple4)] The cat sees the mouse.[(triple5)] The cat sees the tiger.[(triple6)] The mouse chases the cat.[(triple7)] The mouse needs the tiger.[(triple8)] The mouse sees the cat.[(triple9)] The mouse sees the tiger.[(triple10)] The tiger chases the cat.[(triple11)] The tiger is green.[(triple12)] The tiger needs the mouse.[(triple13)] The tiger sees the cat.[(triple14)] The tiger sees the mouse.[(triple15)] @1: The tiger is young.[(((triple2) -> rule2))]
The cat chases the mouse.
("cat" "chases" "mouse" "+")
triple1
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple2
The cat is green.
("cat" "is" "green" "+")
triple3
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple4
The cat sees the mouse.
("cat" "sees" "mouse" "+")
triple5
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple6
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple7
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple8
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple9
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple10
The tiger chases the cat.
("tiger" "chases" "cat" "+")
triple11
The tiger is green.
("tiger" "is" "green" "+")
triple12
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple13
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple14
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple15
The tiger is young.
("tiger" "is" "young" "+")
((triple2) -> (rule2 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1