The cat eats the lion. The lion eats the cat. The lion needs the cat. If someone eats the cat and they visit the cat then the cat visits the lion. If someone visits the lion and the lion visits the cat then they are green. If someone visits the lion and the lion visits the cat then the cat needs the lion. If someone needs the lion and they need the cat then the cat is blue. If someone eats the lion then the lion visits the cat. If someone visits the lion and they need the lion then they eat the cat.
The cat eats the lion.
("cat" "eats" "lion" "+")
The lion eats the cat.
("lion" "eats" "cat" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
If someone eats the cat and they visit the cat then the cat visits the lion.
((("someone" "eats" "cat" "+") ("someone" "visits" "cat" "+")) -> ("cat" "visits" "lion" "+"))
If someone visits the lion and the lion visits the cat then they are green.
((("someone" "visits" "lion" "+") ("lion" "visits" "cat" "+")) -> ("someone" "is" "green" "+"))
If someone visits the lion and the lion visits the cat then the cat needs the lion.
((("someone" "visits" "lion" "+") ("lion" "visits" "cat" "+")) -> ("cat" "needs" "lion" "+"))
If someone needs the lion and they need the cat then the cat is blue.
((("someone" "needs" "lion" "+") ("someone" "needs" "cat" "+")) -> ("cat" "is" "blue" "+"))
If someone eats the lion then the lion visits the cat.
((("someone" "eats" "lion" "+")) -> ("lion" "visits" "cat" "+"))
If someone visits the lion and they need the lion then they eat the cat.
((("someone" "visits" "lion" "+") ("someone" "needs" "lion" "+")) -> ("someone" "eats" "cat" "+"))
The lion needs the cat.
True
1
proof
[(triple3)]
("lion" "needs" "cat" "+")
triple3
The cat does not eat the lion.
False
1
inv-proof
[(triple1)]
("cat" "eats" "lion" "-")
triple1
The lion visits the cat.
True
2
proof
[(((triple1) -> rule5))]
("lion" "visits" "cat" "+")
((triple1) -> (rule5 % int1))
The lion visits the cat.
("lion" "visits" "cat" "+")
int1
The lion does not visit the cat.
False
2
inv-proof
[(((triple1) -> rule5))]
("lion" "visits" "cat" "-")
((triple1) -> (rule5 % int1))
The lion visits the cat.
("lion" "visits" "cat" "+")
int1
The cat visits the lion.
True
4
proof
[(((triple2 ((triple1) -> rule5)) -> rule1))]
("cat" "visits" "lion" "+")
((triple2 ((triple1) -> (rule5 % int2))) -> (rule1 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
int2
The cat does not visit the lion.
False
4
inv-proof
[(((triple2 ((triple1) -> rule5)) -> rule1))]
("cat" "visits" "lion" "-")
((triple2 ((triple1) -> (rule5 % int2))) -> (rule1 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
int2
The cat needs the lion.
True
7
proof
[(((((triple2 ((triple1) -> rule5)) -> rule1) ((triple1) -> rule5)) -> rule3))]
("cat" "needs" "lion" "+")
((((triple2 ((triple1) -> (rule5 % int3))) -> (rule1 % int2)) ((triple1) -> (rule5 % int3))) -> (rule3 % int1))
The cat needs the lion.
("cat" "needs" "lion" "+")
int1
The cat visits the lion.
("cat" "visits" "lion" "+")
int2
The lion visits the cat.
("lion" "visits" "cat" "+")
int3
The cat is not green.
False
7
inv-proof
[(((((triple2 ((triple1) -> rule5)) -> rule1) ((triple1) -> rule5)) -> rule2))]
("cat" "is" "green" "-")
((((triple2 ((triple1) -> (rule5 % int3))) -> (rule1 % int2)) ((triple1) -> (rule5 % int3))) -> (rule2 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat visits the lion.
("cat" "visits" "lion" "+")
int2
The lion visits the cat.
("lion" "visits" "cat" "+")
int3
The cat is not blue.
Unknown
inv-rconc
[@1: The cat is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "is" "blue" "-")
The lion is green.
Unknown
rconc
[@1: The lion is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "is" "green" "+")
The lion is not cold.
Unknown
inv-random
[@0: The lion is cold.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "cold" "-")
The cat is kind.
Unknown
random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "+")
The lion does not eat the lion.
Unknown
inv-random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "-")
The lion is rough.
Unknown
random
[@0: The lion is rough.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "rough" "+")
The cat does not visit the cat.
Unknown
inv-random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "-")
The lion is kind.
Unknown
random
[@0: The lion is kind.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "kind" "+")
@0: The cat eats the lion.[(triple1)] The lion eats the cat.[(triple2)] The lion needs the cat.[(triple3)] @1: The lion visits the cat.[(((triple1) -> rule5))] @2: The cat visits the lion.[(((triple2 ((triple1) -> rule5)) -> rule1))] @3: The cat is green.[(((((triple2 ((triple1) -> rule5)) -> rule1) ((triple1) -> rule5)) -> rule2))] The cat needs the lion.[(((((triple2 ((triple1) -> rule5)) -> rule1) ((triple1) -> rule5)) -> rule3))] @4: The cat eats the cat.[(((((triple2 ((triple1) -> rule5)) -> rule1) ((((triple2 ((triple1) -> rule5)) -> rule1) ((triple1) -> rule5)) -> rule3)) -> rule6))]
The cat eats the lion.
("cat" "eats" "lion" "+")
triple1
The lion eats the cat.
("lion" "eats" "cat" "+")
triple2
The lion needs the cat.
("lion" "needs" "cat" "+")
triple3
The lion visits the cat.
("lion" "visits" "cat" "+")
((triple1) -> (rule5 % int1))
The lion visits the cat.
("lion" "visits" "cat" "+")
int1
The cat visits the lion.
("cat" "visits" "lion" "+")
((triple2 ((triple1) -> (rule5 % int2))) -> (rule1 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
int2
The cat is green.
("cat" "is" "green" "+")
((((triple2 ((triple1) -> (rule5 % int3))) -> (rule1 % int2)) ((triple1) -> (rule5 % int3))) -> (rule2 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat visits the lion.
("cat" "visits" "lion" "+")
int2
The lion visits the cat.
("lion" "visits" "cat" "+")
int3
The cat needs the lion.
("cat" "needs" "lion" "+")
((((triple2 ((triple1) -> (rule5 % int3))) -> (rule1 % int2)) ((triple1) -> (rule5 % int3))) -> (rule3 % int1))
The cat needs the lion.
("cat" "needs" "lion" "+")
int1
The cat visits the lion.
("cat" "visits" "lion" "+")
int2
The lion visits the cat.
("lion" "visits" "cat" "+")
int3
The cat eats the cat.
("cat" "eats" "cat" "+")
((((triple2 ((triple1) -> (rule5 % int4))) -> (rule1 % int3)) ((((triple2 ((triple1) -> (rule5 % int4))) -> (rule1 % int3)) ((triple1) -> (rule5 % int4))) -> (rule3 % int2))) -> (rule6 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
int2
The cat visits the lion.
("cat" "visits" "lion" "+")
int3
The lion visits the cat.
("lion" "visits" "cat" "+")
int4