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