The dog does not eat the lion. The lion is cold. The tiger needs the dog. If someone needs the dog and they need the lion then they visit the tiger. If someone is kind and they need the lion then they visit the tiger. If the lion is young and the lion is not green then the lion eats the dog. If someone is young and they visit the lion then the lion does not visit the tiger. If someone needs the dog then they need the tiger. If someone needs the tiger then the tiger needs the lion. If someone needs the tiger then they need the lion. If someone is young and they do not need the tiger then they eat the dog.
The dog does not eat the lion.
("dog" "eats" "lion" "-")
The lion is cold.
("lion" "is" "cold" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
If someone needs the dog and they need the lion then they visit the tiger.
((("someone" "needs" "dog" "+") ("someone" "needs" "lion" "+")) -> ("someone" "visits" "tiger" "+"))
If someone is kind and they need the lion then they visit the tiger.
((("someone" "is" "kind" "+") ("someone" "needs" "lion" "+")) -> ("someone" "visits" "tiger" "+"))
If the lion is young and the lion is not green then the lion eats the dog.
((("lion" "is" "young" "+") ("lion" "is" "green" "~")) -> ("lion" "eats" "dog" "+"))
If someone is young and they visit the lion then the lion does not visit the tiger.
((("someone" "is" "young" "+") ("someone" "visits" "lion" "+")) -> ("lion" "visits" "tiger" "-"))
If someone needs the dog then they need the tiger.
((("someone" "needs" "dog" "+")) -> ("someone" "needs" "tiger" "+"))
If someone needs the tiger then the tiger needs the lion.
((("someone" "needs" "tiger" "+")) -> ("tiger" "needs" "lion" "+"))
If someone needs the tiger then they need the lion.
((("someone" "needs" "tiger" "+")) -> ("someone" "needs" "lion" "+"))
If someone is young and they do not need the tiger then they eat the dog.
((("someone" "is" "young" "+") ("someone" "needs" "tiger" "~")) -> ("someone" "eats" "dog" "+"))
The lion is cold.
True
1
proof
[(triple2)]
("lion" "is" "cold" "+")
triple2
The lion is not cold.
False
1
inv-proof
[(triple2)]
("lion" "is" "cold" "-")
triple2
The tiger needs the tiger.
True
2
proof
[(((triple3) -> rule5))]
("tiger" "needs" "tiger" "+")
((triple3) -> (rule5 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger does not need the tiger.
False
2
inv-proof
[(((triple3) -> rule5))]
("tiger" "needs" "tiger" "-")
((triple3) -> (rule5 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger needs the lion.
True
3
proof
[(((((triple3) -> rule5)) -> rule6) OR ((((triple3) -> rule5)) -> rule7))]
("tiger" "needs" "lion" "+")
((((triple3) -> (rule5 % int2))) -> (rule6 % int1))
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
((((triple3) -> (rule5 % int2))) -> (rule7 % int1))
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
The tiger does not need the lion.
False
3
inv-proof
[(((((triple3) -> rule5)) -> rule6) OR ((((triple3) -> rule5)) -> rule7))]
("tiger" "needs" "lion" "-")
((((triple3) -> (rule5 % int2))) -> (rule6 % int1))
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
((((triple3) -> (rule5 % int2))) -> (rule7 % int1))
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
The tiger visits the tiger.
True
5
proof
[(((triple3 ((((triple3) -> rule5)) -> rule6)) -> rule1) OR ((triple3 ((((triple3) -> rule5)) -> rule7)) -> rule1))]
("tiger" "visits" "tiger" "+")
((triple3 ((((triple3) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int2
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int3
((triple3 ((((triple3) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int2
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int3
The tiger does not visit the tiger.
False
5
inv-proof
[(((triple3 ((((triple3) -> rule5)) -> rule6)) -> rule1) OR ((triple3 ((((triple3) -> rule5)) -> rule7)) -> rule1))]
("tiger" "visits" "tiger" "-")
((triple3 ((((triple3) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int2
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int3
((triple3 ((((triple3) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int2
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int3
The lion does not need the lion.
Unknown
inv-rconc
[@2: The lion needs the lion.[CWA. Example of deepest failure = (rule7 <- rule5 <- FAIL)]]
("lion" "needs" "lion" "-")
The lion needs the tiger.
Unknown
rconc
[@1: The lion needs the tiger.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "needs" "tiger" "+")
The lion does not eat the dog.
Unknown
inv-rconc
[@1: The lion eats the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "eats" "dog" "-")
The dog eats the dog.
Unknown
rconc
[@1: The dog eats the dog.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("dog" "eats" "dog" "+")
The lion does not visit the dog.
Unknown
inv-random
[@0: The lion visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "dog" "-")
The tiger is cold.
Unknown
random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "+")
The lion is not green.
Unknown
inv-random
[@0: The lion is green.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "green" "-")
The tiger visits the lion.
Unknown
random
[@0: The tiger visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "lion" "+")
@0: The dog does not eat the lion.[(triple1)] The lion is cold.[(triple2)] The tiger needs the dog.[(triple3)] @1: The tiger needs the tiger.[(((triple3) -> rule5))] @2: The tiger needs the lion.[(((((triple3) -> rule5)) -> rule6) OR ((((triple3) -> rule5)) -> rule7))] @3: The tiger visits the tiger.[(((triple3 ((((triple3) -> rule5)) -> rule6)) -> rule1) OR ((triple3 ((((triple3) -> rule5)) -> rule7)) -> rule1))]
The dog does not eat the lion.
("dog" "eats" "lion" "-")
triple1
The lion is cold.
("lion" "is" "cold" "+")
triple2
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple3
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
((triple3) -> (rule5 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger needs the lion.
("tiger" "needs" "lion" "+")
((((triple3) -> (rule5 % int2))) -> (rule6 % int1))
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
((((triple3) -> (rule5 % int2))) -> (rule7 % int1))
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
((triple3 ((((triple3) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int2
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int3
((triple3 ((((triple3) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int2
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int3