The cat chases the tiger. The cat eats the squirrel. The cat is green. The cat is kind. The cat is young. The cat needs the squirrel. The cat needs the tiger. The squirrel chases the tiger. The squirrel is blue. The tiger eats the cat. The tiger eats the squirrel. The tiger does not need the squirrel. If the cat chases the squirrel then the cat is kind. If something eats the tiger then it does not chase the tiger. If something needs the cat then the cat needs the squirrel. If something needs the squirrel and the squirrel chases the cat then the cat needs the squirrel. If something needs the cat and it is not rough then the cat needs the squirrel. If something is kind and it does not need the cat then the cat needs the squirrel. If something chases the squirrel then it is not young. If something is blue then it chases the squirrel.
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is young.
("cat" "is" "young" "+")
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The tiger eats the cat.
("tiger" "eats" "cat" "+")
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
The tiger does not need the squirrel.
("tiger" "needs" "squirrel" "-")
If the cat chases the squirrel then the cat is kind.
((("cat" "chases" "squirrel" "+")) -> ("cat" "is" "kind" "+"))
If something eats the tiger then it does not chase the tiger.
((("something" "eats" "tiger" "+")) -> ("something" "chases" "tiger" "-"))
If something needs the cat then the cat needs the squirrel.
((("something" "needs" "cat" "+")) -> ("cat" "needs" "squirrel" "+"))
If something needs the squirrel and the squirrel chases the cat then the cat needs the squirrel.
((("something" "needs" "squirrel" "+") ("squirrel" "chases" "cat" "+")) -> ("cat" "needs" "squirrel" "+"))
If something needs the cat and it is not rough then the cat needs the squirrel.
((("something" "needs" "cat" "+") ("something" "is" "rough" "~")) -> ("cat" "needs" "squirrel" "+"))
If something is kind and it does not need the cat then the cat needs the squirrel.
((("something" "is" "kind" "+") ("something" "needs" "cat" "~")) -> ("cat" "needs" "squirrel" "+"))
If something chases the squirrel then it is not young.
((("something" "chases" "squirrel" "+")) -> ("something" "is" "young" "-"))
If something is blue then it chases the squirrel.
((("something" "is" "blue" "+")) -> ("something" "chases" "squirrel" "+"))
The cat chases the tiger.
True
1
proof
[(triple1)]
("cat" "chases" "tiger" "+")
triple1
The cat does not chase the tiger.
False
1
inv-proof
[(triple1)]
("cat" "chases" "tiger" "-")
triple1
The cat does not chase the squirrel.
Unknown
inv-rconc
[@1: The cat chases the squirrel.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cat" "chases" "squirrel" "-")
The cat needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
@0: The cat chases the tiger.[(triple1)] The cat eats the squirrel.[(triple2)] The cat is green.[(triple3)] The cat is kind.[(triple4)] The cat is young.[(triple5)] The cat needs the squirrel.[(triple6)] The cat needs the tiger.[(triple7)] The squirrel chases the tiger.[(triple8)] The squirrel is blue.[(triple9)] The tiger does not need the squirrel.[(triple12)] The tiger eats the cat.[(triple10)] The tiger eats the squirrel.[(triple11)] @1: The squirrel chases the squirrel.[(((triple9) -> rule8))] @2: The squirrel is not young.[(((((triple9) -> rule8)) -> rule7))]
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple1
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
triple2
The cat is green.
("cat" "is" "green" "+")
triple3
The cat is kind.
("cat" "is" "kind" "+")
triple4
The cat is young.
("cat" "is" "young" "+")
triple5
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
triple6
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple7
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
triple8
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple9
The tiger does not need the squirrel.
("tiger" "needs" "squirrel" "-")
triple12
The tiger eats the cat.
("tiger" "eats" "cat" "+")
triple10
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
triple11
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
((triple9) -> (rule8 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel is not young.
("squirrel" "is" "young" "-")
((((triple9) -> (rule8 % int2))) -> (rule7 % int1))
The squirrel is not young.
("squirrel" "is" "young" "-")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int2