The cat chases the tiger. The cat is rough. The cat needs the tiger. The cat sees the tiger. The tiger chases the cat. The tiger is cold. The tiger is green. The tiger is kind. The tiger is rough. The tiger is young. The tiger needs the cat. The tiger sees the cat. If something chases the cat then the cat is kind.
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The tiger chases the cat.
("tiger" "chases" "cat" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
If something chases the cat then the cat is kind.
((("something" "chases" "cat" "+")) -> ("cat" "is" "kind" "+"))
The cat needs the tiger.
True
1
proof
[(triple3)]
("cat" "needs" "tiger" "+")
triple3
The tiger does not need the cat.
False
1
inv-proof
[(triple11)]
("tiger" "needs" "cat" "-")
triple11
The cat is not cold.
Unknown
inv-random
[@0: The cat is cold.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "cold" "-")
The cat chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
@0: The cat chases the tiger.[(triple1)] The cat is rough.[(triple2)] The cat needs the tiger.[(triple3)] The cat sees the tiger.[(triple4)] The tiger chases the cat.[(triple5)] The tiger is cold.[(triple6)] The tiger is green.[(triple7)] The tiger is kind.[(triple8)] The tiger is rough.[(triple9)] The tiger is young.[(triple10)] The tiger needs the cat.[(triple11)] The tiger sees the cat.[(triple12)] @1: The cat is kind.[(((triple5) -> rule1))]
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple1
The cat is rough.
("cat" "is" "rough" "+")
triple2
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple3
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple4
The tiger chases the cat.
("tiger" "chases" "cat" "+")
triple5
The tiger is cold.
("tiger" "is" "cold" "+")
triple6
The tiger is green.
("tiger" "is" "green" "+")
triple7
The tiger is kind.
("tiger" "is" "kind" "+")
triple8
The tiger is rough.
("tiger" "is" "rough" "+")
triple9
The tiger is young.
("tiger" "is" "young" "+")
triple10
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple11
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple12
The cat is kind.
("cat" "is" "kind" "+")
((triple5) -> (rule1 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1