The cat needs the lion. The lion is cold. The tiger does not visit the cat. If someone needs the tiger and they are cold then the tiger does not chase the lion. If someone needs the lion then the lion needs the tiger.
The cat needs the lion.
("cat" "needs" "lion" "+")
The lion is cold.
("lion" "is" "cold" "+")
The tiger does not visit the cat.
("tiger" "visits" "cat" "-")
If someone needs the tiger and they are cold then the tiger does not chase the lion.
((("someone" "needs" "tiger" "+") ("someone" "is" "cold" "+")) -> ("tiger" "chases" "lion" "-"))
If someone needs the lion then the lion needs the tiger.
((("someone" "needs" "lion" "+")) -> ("lion" "needs" "tiger" "+"))
The tiger does not visit the cat.
True
1
proof
[(triple3)]
("tiger" "visits" "cat" "-")
triple3
The tiger visits the cat.
False
1
inv-proof
[(triple3)]
("tiger" "visits" "cat" "+")
triple3
The lion needs the tiger.
True
2
proof
[(((triple1) -> rule2))]
("lion" "needs" "tiger" "+")
((triple1) -> (rule2 % int1))
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int1
The lion does not need the tiger.
False
2
inv-proof
[(((triple1) -> rule2))]
("lion" "needs" "tiger" "-")
((triple1) -> (rule2 % int1))
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int1
The tiger does not chase the lion.
True
4
proof
[(((((triple1) -> rule2) triple2) -> rule1))]
("tiger" "chases" "lion" "-")
((((triple1) -> (rule2 % int2)) triple2) -> (rule1 % int1))
The tiger does not chase the lion.
("tiger" "chases" "lion" "-")
int1
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int2
The tiger chases the lion.
False
4
inv-proof
[(((((triple1) -> rule2) triple2) -> rule1))]
("tiger" "chases" "lion" "+")
((((triple1) -> (rule2 % int2)) triple2) -> (rule1 % int1))
The tiger does not chase the lion.
("tiger" "chases" "lion" "-")
int1
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int2
The cat is not cold.
Unknown
inv-random
[@0: The cat is cold.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "cold" "-")
The lion chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
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 tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
The cat does not chase the cat.
Unknown
inv-random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "-")
The tiger needs the cat.
Unknown
random
[@0: The tiger needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "cat" "+")
@0: The cat needs the lion.[(triple1)] The lion is cold.[(triple2)] The tiger does not visit the cat.[(triple3)] @1: The lion needs the tiger.[(((triple1) -> rule2))] @2: The tiger does not chase the lion.[(((((triple1) -> rule2) triple2) -> rule1))]
The cat needs the lion.
("cat" "needs" "lion" "+")
triple1
The lion is cold.
("lion" "is" "cold" "+")
triple2
The tiger does not visit the cat.
("tiger" "visits" "cat" "-")
triple3
The lion needs the tiger.
("lion" "needs" "tiger" "+")
((triple1) -> (rule2 % int1))
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int1
The tiger does not chase the lion.
("tiger" "chases" "lion" "-")
((((triple1) -> (rule2 % int2)) triple2) -> (rule1 % int1))
The tiger does not chase the lion.
("tiger" "chases" "lion" "-")
int1
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int2