The lion needs the tiger. The tiger is blue. The tiger is green. If something needs the lion and the lion chases the tiger then it is not big. If the lion needs the tiger and the lion chases the tiger then the lion visits the tiger. If something is big and it does not visit the lion then the lion does not visit the tiger. If something is nice then it does not need the tiger. If the lion needs the tiger then the lion chases the tiger. If something visits the tiger then the tiger chases the lion.
The lion needs the tiger.
("lion" "needs" "tiger" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is green.
("tiger" "is" "green" "+")
If something needs the lion and the lion chases the tiger then it is not big.
((("something" "needs" "lion" "+") ("lion" "chases" "tiger" "+")) -> ("something" "is" "big" "-"))
If the lion needs the tiger and the lion chases the tiger then the lion visits the tiger.
((("lion" "needs" "tiger" "+") ("lion" "chases" "tiger" "+")) -> ("lion" "visits" "tiger" "+"))
If something is big and it does not visit the lion then the lion does not visit the tiger.
((("something" "is" "big" "+") ("something" "visits" "lion" "~")) -> ("lion" "visits" "tiger" "-"))
If something is nice then it does not need the tiger.
((("something" "is" "nice" "+")) -> ("something" "needs" "tiger" "-"))
If the lion needs the tiger then the lion chases the tiger.
((("lion" "needs" "tiger" "+")) -> ("lion" "chases" "tiger" "+"))
If something visits the tiger then the tiger chases the lion.
((("something" "visits" "tiger" "+")) -> ("tiger" "chases" "lion" "+"))
The tiger is green.
True
1
proof
[(triple3)]
("tiger" "is" "green" "+")
triple3
The tiger is not green.
False
1
inv-proof
[(triple3)]
("tiger" "is" "green" "-")
triple3
The lion chases the tiger.
True
2
proof
[(((triple1) -> rule5))]
("lion" "chases" "tiger" "+")
((triple1) -> (rule5 % int1))
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int1
The lion does not chase the tiger.
False
2
inv-proof
[(((triple1) -> rule5))]
("lion" "chases" "tiger" "-")
((triple1) -> (rule5 % int1))
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int1
The lion visits the tiger.
True
4
proof
[(((triple1 ((triple1) -> rule5)) -> rule2))]
("lion" "visits" "tiger" "+")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule2 % int1))
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int1
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int2
The lion does not visit the tiger.
False
4
inv-proof
[(((triple1 ((triple1) -> rule5)) -> rule2))]
("lion" "visits" "tiger" "-")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule2 % int1))
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int1
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int2
The tiger chases the lion.
True
5
proof
[(((((triple1 ((triple1) -> rule5)) -> rule2)) -> rule6))]
("tiger" "chases" "lion" "+")
((((triple1 ((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int1
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int2
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int3
The tiger does not chase the lion.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule5)) -> rule2)) -> rule6))]
("tiger" "chases" "lion" "-")
((((triple1 ((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int1
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int2
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int3
The tiger is not young.
Unknown
inv-random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "-")
The lion visits the lion.
Unknown
random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "+")
The lion is not big.
Unknown
inv-random
[@0: The lion is big.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "big" "-")
The tiger is big.
Unknown
random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "+")
The tiger does not visit the tiger.
Unknown
inv-random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "-")
The tiger needs the lion.
Unknown
random
[@0: The tiger needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "lion" "+")
The lion is not young.
Unknown
inv-random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "-")
The tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
@0: The lion needs the tiger.[(triple1)] The tiger is blue.[(triple2)] The tiger is green.[(triple3)] @1: The lion chases the tiger.[(((triple1) -> rule5))] @2: The lion visits the tiger.[(((triple1 ((triple1) -> rule5)) -> rule2))] @3: The tiger chases the lion.[(((((triple1 ((triple1) -> rule5)) -> rule2)) -> rule6))]
The lion needs the tiger.
("lion" "needs" "tiger" "+")
triple1
The tiger is blue.
("tiger" "is" "blue" "+")
triple2
The tiger is green.
("tiger" "is" "green" "+")
triple3
The lion chases the tiger.
("lion" "chases" "tiger" "+")
((triple1) -> (rule5 % int1))
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int1
The lion visits the tiger.
("lion" "visits" "tiger" "+")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule2 % int1))
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int1
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int2
The tiger chases the lion.
("tiger" "chases" "lion" "+")
((((triple1 ((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int1
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int2
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int3