The dog chases the tiger. The dog does not see the lion. The lion chases the tiger. The lion is not red. The squirrel chases the lion. The squirrel chases the tiger. The squirrel is blue. The tiger does not chase the dog. The tiger chases the lion. The tiger is big. The tiger does not need the lion. The tiger sees the lion. If someone is rough and they see the tiger then they are green. If the tiger chases the dog and the tiger sees the lion then the lion needs the dog. If someone needs the squirrel and the squirrel sees the lion then they are big. If someone is green then they see the squirrel. If someone is big then they do not chase the tiger. If the dog is big then the dog does not see the squirrel. If someone is red and they do not see the lion then the lion is not big. If someone is red and they do not need the lion then the lion needs the tiger.
The dog chases the tiger.
("dog" "chases" "tiger" "+")
The dog does not see the lion.
("dog" "sees" "lion" "-")
The lion chases the tiger.
("lion" "chases" "tiger" "+")
The lion is not red.
("lion" "is" "red" "-")
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The tiger does not chase the dog.
("tiger" "chases" "dog" "-")
The tiger chases the lion.
("tiger" "chases" "lion" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger does not need the lion.
("tiger" "needs" "lion" "-")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
If someone is rough and they see the tiger then they are green.
((("someone" "is" "rough" "+") ("someone" "sees" "tiger" "+")) -> ("someone" "is" "green" "+"))
If the tiger chases the dog and the tiger sees the lion then the lion needs the dog.
((("tiger" "chases" "dog" "+") ("tiger" "sees" "lion" "+")) -> ("lion" "needs" "dog" "+"))
If someone needs the squirrel and the squirrel sees the lion then they are big.
((("someone" "needs" "squirrel" "+") ("squirrel" "sees" "lion" "+")) -> ("someone" "is" "big" "+"))
If someone is green then they see the squirrel.
((("someone" "is" "green" "+")) -> ("someone" "sees" "squirrel" "+"))
If someone is big then they do not chase the tiger.
((("someone" "is" "big" "+")) -> ("someone" "chases" "tiger" "-"))
If the dog is big then the dog does not see the squirrel.
((("dog" "is" "big" "+")) -> ("dog" "sees" "squirrel" "-"))
If someone is red and they do not see the lion then the lion is not big.
((("someone" "is" "red" "+") ("someone" "sees" "lion" "~")) -> ("lion" "is" "big" "-"))
If someone is red and they do not need the lion then the lion needs the tiger.
((("someone" "is" "red" "+") ("someone" "needs" "lion" "~")) -> ("lion" "needs" "tiger" "+"))
The tiger sees the lion.
True
1
proof
[(triple12)]
("tiger" "sees" "lion" "+")
triple12
The tiger needs the lion.
False
1
inv-proof
[(triple11)]
("tiger" "needs" "lion" "+")
triple11
The tiger does not chase the tiger.
True
2
proof
[(((triple10) -> rule5))]
("tiger" "chases" "tiger" "-")
((triple10) -> (rule5 % int1))
The tiger does not chase the tiger.
("tiger" "chases" "tiger" "-")
int1
The tiger chases the tiger.
False
2
inv-proof
[(((triple10) -> rule5))]
("tiger" "chases" "tiger" "+")
((triple10) -> (rule5 % int1))
The tiger does not chase the tiger.
("tiger" "chases" "tiger" "-")
int1
The lion does not need the tiger.
Unknown
inv-rconc
[@1: The lion needs the tiger.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("lion" "needs" "tiger" "-")
The tiger sees the squirrel.
Unknown
rconc
[@2: The tiger sees the squirrel.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("tiger" "sees" "squirrel" "+")
The dog is not blue.
Unknown
inv-random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "-")
The tiger is blue.
Unknown
random
[@0: The tiger is blue.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "blue" "+")
@0: The dog chases the tiger.[(triple1)] The dog does not see the lion.[(triple2)] The lion chases the tiger.[(triple3)] The lion is not red.[(triple4)] The squirrel chases the lion.[(triple5)] The squirrel chases the tiger.[(triple6)] The squirrel is blue.[(triple7)] The tiger chases the lion.[(triple9)] The tiger does not chase the dog.[(triple8)] The tiger does not need the lion.[(triple11)] The tiger is big.[(triple10)] The tiger sees the lion.[(triple12)] @1: The tiger does not chase the tiger.[(((triple10) -> rule5))]
The dog chases the tiger.
("dog" "chases" "tiger" "+")
triple1
The dog does not see the lion.
("dog" "sees" "lion" "-")
triple2
The lion chases the tiger.
("lion" "chases" "tiger" "+")
triple3
The lion is not red.
("lion" "is" "red" "-")
triple4
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
triple5
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
triple6
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple7
The tiger chases the lion.
("tiger" "chases" "lion" "+")
triple9
The tiger does not chase the dog.
("tiger" "chases" "dog" "-")
triple8
The tiger does not need the lion.
("tiger" "needs" "lion" "-")
triple11
The tiger is big.
("tiger" "is" "big" "+")
triple10
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple12
The tiger does not chase the tiger.
("tiger" "chases" "tiger" "-")
((triple10) -> (rule5 % int1))
The tiger does not chase the tiger.
("tiger" "chases" "tiger" "-")
int1