The cat needs the lion. The lion sees the cat. The tiger is not cold. If something visits the cat and it is not nice then it does not need the tiger. If something is young and it visits the tiger then it needs the tiger. If something sees the cat then it needs the tiger. If something is blue then it is big. If something visits the lion then it sees the cat. If something needs the tiger then it sees the tiger. If something sees the tiger then it is young. If something visits the lion and the lion sees the cat then it visits the tiger.
The cat needs the lion.
("cat" "needs" "lion" "+")
The lion sees the cat.
("lion" "sees" "cat" "+")
The tiger is not cold.
("tiger" "is" "cold" "-")
If something visits the cat and it is not nice then it does not need the tiger.
((("something" "visits" "cat" "+") ("something" "is" "nice" "~")) -> ("something" "needs" "tiger" "-"))
If something is young and it visits the tiger then it needs the tiger.
((("something" "is" "young" "+") ("something" "visits" "tiger" "+")) -> ("something" "needs" "tiger" "+"))
If something sees the cat then it needs the tiger.
((("something" "sees" "cat" "+")) -> ("something" "needs" "tiger" "+"))
If something is blue then it is big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
If something visits the lion then it sees the cat.
((("something" "visits" "lion" "+")) -> ("something" "sees" "cat" "+"))
If something needs the tiger then it sees the tiger.
((("something" "needs" "tiger" "+")) -> ("something" "sees" "tiger" "+"))
If something sees the tiger then it is young.
((("something" "sees" "tiger" "+")) -> ("something" "is" "young" "+"))
If something visits the lion and the lion sees the cat then it visits the tiger.
((("something" "visits" "lion" "+") ("lion" "sees" "cat" "+")) -> ("something" "visits" "tiger" "+"))
The cat needs the lion.
True
1
proof
[(triple1)]
("cat" "needs" "lion" "+")
triple1
The cat does not need the lion.
False
1
inv-proof
[(triple1)]
("cat" "needs" "lion" "-")
triple1
The lion needs the tiger.
True
2
proof
[(((triple2) -> rule3))]
("lion" "needs" "tiger" "+")
((triple2) -> (rule3 % int1))
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int1
The lion does not need the tiger.
False
2
inv-proof
[(((triple2) -> rule3))]
("lion" "needs" "tiger" "-")
((triple2) -> (rule3 % int1))
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int1
The lion sees the tiger.
True
3
proof
[(((((triple2) -> rule3)) -> rule6))]
("lion" "sees" "tiger" "+")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int2
The lion does not see the tiger.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule6))]
("lion" "sees" "tiger" "-")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int2
The tiger is not young.
Unknown
inv-rconc
[@4: The tiger is young.[CWA. Example of deepest failure = (rule7 <- rule6 <- rule3 <- rule5 <- FAIL)]]
("tiger" "is" "young" "-")
The cat is big.
Unknown
rconc
[@1: The cat is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "is" "big" "+")
The cat does not see the cat.
Unknown
inv-rconc
[@1: The cat sees the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "sees" "cat" "-")
The cat is nice.
Unknown
random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "+")
The lion is not cold.
Unknown
inv-random
[@0: The lion is cold.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "cold" "-")
The lion visits the lion.
Unknown
random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "+")
@0: The cat needs the lion.[(triple1)] The lion sees the cat.[(triple2)] The tiger is not cold.[(triple3)] @1: The lion needs the tiger.[(((triple2) -> rule3))] @2: The lion sees the tiger.[(((((triple2) -> rule3)) -> rule6))] @3: The lion is young.[(((((((triple2) -> rule3)) -> rule6)) -> rule7))]
The cat needs the lion.
("cat" "needs" "lion" "+")
triple1
The lion sees the cat.
("lion" "sees" "cat" "+")
triple2
The tiger is not cold.
("tiger" "is" "cold" "-")
triple3
The lion needs the tiger.
("lion" "needs" "tiger" "+")
((triple2) -> (rule3 % int1))
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int2
The lion is young.
("lion" "is" "young" "+")
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int2
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int3