The cat is not green. The cat sees the lion. The lion eats the tiger. The lion is big. The tiger is not cold. The tiger is nice. The tiger likes the cat. If something likes the lion and it eats the cat then the lion likes the tiger. If something likes the lion and it is big then the lion does not like the tiger. If something is nice and it does not eat the tiger then it does not see the tiger. If something sees the lion and it likes the tiger then the lion sees the cat. If something likes the cat then it is round. If something is big and it eats the tiger then the tiger sees the cat. If the cat is green then the cat is big. If the tiger is round and the tiger is nice then the tiger likes the lion.
The cat is not green.
("cat" "is" "green" "-")
The cat sees the lion.
("cat" "sees" "lion" "+")
The lion eats the tiger.
("lion" "eats" "tiger" "+")
The lion is big.
("lion" "is" "big" "+")
The tiger is not cold.
("tiger" "is" "cold" "-")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger likes the cat.
("tiger" "likes" "cat" "+")
If something likes the lion and it eats the cat then the lion likes the tiger.
((("something" "likes" "lion" "+") ("something" "eats" "cat" "+")) -> ("lion" "likes" "tiger" "+"))
If something likes the lion and it is big then the lion does not like the tiger.
((("something" "likes" "lion" "+") ("something" "is" "big" "+")) -> ("lion" "likes" "tiger" "-"))
If something is nice and it does not eat the tiger then it does not see the tiger.
((("something" "is" "nice" "+") ("something" "eats" "tiger" "~")) -> ("something" "sees" "tiger" "-"))
If something sees the lion and it likes the tiger then the lion sees the cat.
((("something" "sees" "lion" "+") ("something" "likes" "tiger" "+")) -> ("lion" "sees" "cat" "+"))
If something likes the cat then it is round.
((("something" "likes" "cat" "+")) -> ("something" "is" "round" "+"))
If something is big and it eats the tiger then the tiger sees the cat.
((("something" "is" "big" "+") ("something" "eats" "tiger" "+")) -> ("tiger" "sees" "cat" "+"))
If the cat is green then the cat is big.
((("cat" "is" "green" "+")) -> ("cat" "is" "big" "+"))
If the tiger is round and the tiger is nice then the tiger likes the lion.
((("tiger" "is" "round" "+") ("tiger" "is" "nice" "+")) -> ("tiger" "likes" "lion" "+"))
The cat is not green.
True
1
proof
[(triple1)]
("cat" "is" "green" "-")
triple1
The cat is green.
False
1
inv-proof
[(triple1)]
("cat" "is" "green" "+")
triple1
The tiger sees the cat.
True
3
proof
[(((triple4 triple3) -> rule6))]
("tiger" "sees" "cat" "+")
((triple4 triple3) -> (rule6 % int1))
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int1
The tiger does not see the cat.
False
3
inv-proof
[(((triple4 triple3) -> rule6))]
("tiger" "sees" "cat" "-")
((triple4 triple3) -> (rule6 % int1))
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int1
The tiger likes the lion.
True
4
proof
[(((((triple7) -> rule5) triple6) -> rule8))]
("tiger" "likes" "lion" "+")
((((triple7) -> (rule5 % int2)) triple6) -> (rule8 % int1))
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The tiger does not like the lion.
False
4
inv-proof
[(((((triple7) -> rule5) triple6) -> rule8))]
("tiger" "likes" "lion" "-")
((((triple7) -> (rule5 % int2)) triple6) -> (rule8 % int1))
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The cat is not big.
Unknown
inv-rconc
[@1: The cat is big.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cat" "is" "big" "-")
The lion likes the tiger.
Unknown
rconc
[@1: The lion likes the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "likes" "tiger" "+")
The lion does not see the cat.
Unknown
inv-rconc
[@1: The lion sees the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "sees" "cat" "-")
The cat is nice.
Unknown
random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "+")
The lion does not see the lion.
Unknown
inv-random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "-")
The lion is cold.
Unknown
random
[@0: The lion is cold.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "cold" "+")
@0: The cat is not green.[(triple1)] The cat sees the lion.[(triple2)] The lion eats the tiger.[(triple3)] The lion is big.[(triple4)] The tiger is nice.[(triple6)] The tiger is not cold.[(triple5)] The tiger likes the cat.[(triple7)] @1: The tiger is round.[(((triple7) -> rule5))] The tiger sees the cat.[(((triple4 triple3) -> rule6))] @2: The tiger likes the lion.[(((((triple7) -> rule5) triple6) -> rule8))]
The cat is not green.
("cat" "is" "green" "-")
triple1
The cat sees the lion.
("cat" "sees" "lion" "+")
triple2
The lion eats the tiger.
("lion" "eats" "tiger" "+")
triple3
The lion is big.
("lion" "is" "big" "+")
triple4
The tiger is nice.
("tiger" "is" "nice" "+")
triple6
The tiger is not cold.
("tiger" "is" "cold" "-")
triple5
The tiger likes the cat.
("tiger" "likes" "cat" "+")
triple7
The tiger is round.
("tiger" "is" "round" "+")
((triple7) -> (rule5 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger sees the cat.
("tiger" "sees" "cat" "+")
((triple4 triple3) -> (rule6 % int1))
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int1
The tiger likes the lion.
("tiger" "likes" "lion" "+")
((((triple7) -> (rule5 % int2)) triple6) -> (rule8 % int1))
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2