The cat is young. The cat needs the tiger. The dog is rough. The mouse chases the dog. The tiger chases the mouse. The tiger is not rough. The tiger needs the dog. If something sees the mouse then it is not kind. If something chases the mouse and the mouse is not big then it sees the cat. If the cat does not see the tiger then the tiger sees the cat. If something sees the mouse and the mouse is red then the mouse does not need the dog. All young things are red. If something needs the tiger and it is rough then the tiger is kind.
The cat is young.
("cat" "is" "young" "+")
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The dog is rough.
("dog" "is" "rough" "+")
The mouse chases the dog.
("mouse" "chases" "dog" "+")
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
The tiger is not rough.
("tiger" "is" "rough" "-")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
If something sees the mouse then it is not kind.
((("something" "sees" "mouse" "+")) -> ("something" "is" "kind" "-"))
If something chases the mouse and the mouse is not big then it sees the cat.
((("something" "chases" "mouse" "+") ("mouse" "is" "big" "~")) -> ("something" "sees" "cat" "+"))
If the cat does not see the tiger then the tiger sees the cat.
((("cat" "sees" "tiger" "~")) -> ("tiger" "sees" "cat" "+"))
If something sees the mouse and the mouse is red then the mouse does not need the dog.
((("something" "sees" "mouse" "+") ("mouse" "is" "red" "+")) -> ("mouse" "needs" "dog" "-"))
All young things are red.
((("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
If something needs the tiger and it is rough then the tiger is kind.
((("something" "needs" "tiger" "+") ("something" "is" "rough" "+")) -> ("tiger" "is" "kind" "+"))
The tiger is not rough.
True
1
proof
[(triple6)]
("tiger" "is" "rough" "-")
triple6
The mouse does not chase the dog.
False
1
inv-proof
[(triple4)]
("mouse" "chases" "dog" "-")
triple4
The cat is red.
True
2
proof
[(((triple1) -> rule5))]
("cat" "is" "red" "+")
((triple1) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is not red.
False
2
inv-proof
[(((triple1) -> rule5))]
("cat" "is" "red" "-")
((triple1) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The dog does not see the cat.
Unknown
inv-rconc
[@1: The dog sees the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "sees" "cat" "-")
The tiger sees the cat.
Unknown
rconc
[@1: The tiger sees the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "sees" "cat" "+")
The mouse is not big.
Unknown
inv-random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "-")
The cat chases the tiger.
Unknown
random
[@0: The cat chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "tiger" "+")
@0: The cat is young.[(triple1)] The cat needs the tiger.[(triple2)] The dog is rough.[(triple3)] The mouse chases the dog.[(triple4)] The tiger chases the mouse.[(triple5)] The tiger is not rough.[(triple6)] The tiger needs the dog.[(triple7)] @1: The cat is red.[(((triple1) -> rule5))]
The cat is young.
("cat" "is" "young" "+")
triple1
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple2
The dog is rough.
("dog" "is" "rough" "+")
triple3
The mouse chases the dog.
("mouse" "chases" "dog" "+")
triple4
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
triple5
The tiger is not rough.
("tiger" "is" "rough" "-")
triple6
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple7
The cat is red.
("cat" "is" "red" "+")
((triple1) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1