The dog is cold. The dog is red. The dog does not need the mouse. The lion is cold. The lion needs the mouse. The lion needs the tiger. The lion sees the tiger. The mouse is red. The tiger is cold. The tiger is not nice. If someone eats the tiger then they are red. If someone is rough and nice then they do not see the lion. If the mouse needs the dog then the dog needs the tiger. If someone is cold then they do not need the lion. If the mouse eats the dog then the mouse needs the dog. If someone is nice then they eat the lion. If someone eats the lion then the lion is round. If someone sees the tiger and they do not need the lion then the tiger eats the lion.
The dog is cold.
("dog" "is" "cold" "+")
The dog is red.
("dog" "is" "red" "+")
The dog does not need the mouse.
("dog" "needs" "mouse" "-")
The lion is cold.
("lion" "is" "cold" "+")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The lion needs the tiger.
("lion" "needs" "tiger" "+")
The lion sees the tiger.
("lion" "sees" "tiger" "+")
The mouse is red.
("mouse" "is" "red" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is not nice.
("tiger" "is" "nice" "-")
If someone eats the tiger then they are red.
((("someone" "eats" "tiger" "+")) -> ("someone" "is" "red" "+"))
If someone is rough and nice then they do not see the lion.
((("someone" "is" "rough" "+") ("someone" "is" "nice" "+")) -> ("someone" "sees" "lion" "-"))
If the mouse needs the dog then the dog needs the tiger.
((("mouse" "needs" "dog" "+")) -> ("dog" "needs" "tiger" "+"))
If someone is cold then they do not need the lion.
((("someone" "is" "cold" "+")) -> ("someone" "needs" "lion" "-"))
If the mouse eats the dog then the mouse needs the dog.
((("mouse" "eats" "dog" "+")) -> ("mouse" "needs" "dog" "+"))
If someone is nice then they eat the lion.
((("someone" "is" "nice" "+")) -> ("someone" "eats" "lion" "+"))
If someone eats the lion then the lion is round.
((("someone" "eats" "lion" "+")) -> ("lion" "is" "round" "+"))
If someone sees the tiger and they do not need the lion then the tiger eats the lion.
((("someone" "sees" "tiger" "+") ("someone" "needs" "lion" "~")) -> ("tiger" "eats" "lion" "+"))
The tiger is cold.
True
1
proof
[(triple9)]
("tiger" "is" "cold" "+")
triple9
The tiger is not cold.
False
1
inv-proof
[(triple9)]
("tiger" "is" "cold" "-")
triple9
The tiger does not need the lion.
True
2
proof
[(((triple9) -> rule4))]
("tiger" "needs" "lion" "-")
((triple9) -> (rule4 % int1))
The tiger does not need the lion.
("tiger" "needs" "lion" "-")
int1
The dog needs the lion.
False
2
inv-proof
[(((triple1) -> rule4))]
("dog" "needs" "lion" "+")
((triple1) -> (rule4 % int1))
The dog does not need the lion.
("dog" "needs" "lion" "-")
int1
The tiger eats the lion.
True
4
proof
[(((triple7 ((triple4) -> rule4)) -> rule8))]
("tiger" "eats" "lion" "+")
((triple7 ((triple4) -> (rule4 % int2))) -> (rule8 % int1))
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int1
The lion does not need the lion.
("lion" "needs" "lion" "-")
int2
The tiger does not eat the lion.
False
4
inv-proof
[(((triple7 ((triple4) -> rule4)) -> rule8))]
("tiger" "eats" "lion" "-")
((triple7 ((triple4) -> (rule4 % int2))) -> (rule8 % int1))
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int1
The lion does not need the lion.
("lion" "needs" "lion" "-")
int2
The lion is round.
True
5
proof
[(((((triple7 ((triple4) -> rule4)) -> rule8)) -> rule7))]
("lion" "is" "round" "+")
((((triple7 ((triple4) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int2
The lion does not need the lion.
("lion" "needs" "lion" "-")
int3
The lion is not round.
False
5
inv-proof
[(((((triple7 ((triple4) -> rule4)) -> rule8)) -> rule7))]
("lion" "is" "round" "-")
((((triple7 ((triple4) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int2
The lion does not need the lion.
("lion" "needs" "lion" "-")
int3
The tiger is not red.
Unknown
inv-rconc
[@1: The tiger is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "is" "red" "-")
The mouse eats the lion.
Unknown
rconc
[@1: The mouse eats the lion.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "eats" "lion" "+")
The dog does not eat the lion.
Unknown
inv-rconc
[@1: The dog eats the lion.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "eats" "lion" "-")
The dog needs the tiger.
Unknown
rconc
[@2: The dog needs the tiger.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("dog" "needs" "tiger" "+")
The mouse does not see the tiger.
Unknown
inv-random
[@0: The mouse sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "tiger" "-")
The mouse eats the tiger.
Unknown
random
[@0: The mouse eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "tiger" "+")
The mouse does not see the mouse.
Unknown
inv-random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "-")
The tiger sees the dog.
Unknown
random
[@0: The tiger sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "dog" "+")
@0: The dog does not need the mouse.[(triple3)] The dog is cold.[(triple1)] The dog is red.[(triple2)] The lion is cold.[(triple4)] The lion needs the mouse.[(triple5)] The lion needs the tiger.[(triple6)] The lion sees the tiger.[(triple7)] The mouse is red.[(triple8)] The tiger is cold.[(triple9)] The tiger is not nice.[(triple10)] @1: The dog does not need the lion.[(((triple1) -> rule4))] The lion does not need the lion.[(((triple4) -> rule4))] The tiger does not need the lion.[(((triple9) -> rule4))] @2: The tiger eats the lion.[(((triple7 ((triple4) -> rule4)) -> rule8))] @3: The lion is round.[(((((triple7 ((triple4) -> rule4)) -> rule8)) -> rule7))]
The dog does not need the mouse.
("dog" "needs" "mouse" "-")
triple3
The dog is cold.
("dog" "is" "cold" "+")
triple1
The dog is red.
("dog" "is" "red" "+")
triple2
The lion is cold.
("lion" "is" "cold" "+")
triple4
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple5
The lion needs the tiger.
("lion" "needs" "tiger" "+")
triple6
The lion sees the tiger.
("lion" "sees" "tiger" "+")
triple7
The mouse is red.
("mouse" "is" "red" "+")
triple8
The tiger is cold.
("tiger" "is" "cold" "+")
triple9
The tiger is not nice.
("tiger" "is" "nice" "-")
triple10
The dog does not need the lion.
("dog" "needs" "lion" "-")
((triple1) -> (rule4 % int1))
The dog does not need the lion.
("dog" "needs" "lion" "-")
int1
The lion does not need the lion.
("lion" "needs" "lion" "-")
((triple4) -> (rule4 % int1))
The lion does not need the lion.
("lion" "needs" "lion" "-")
int1
The tiger does not need the lion.
("tiger" "needs" "lion" "-")
((triple9) -> (rule4 % int1))
The tiger does not need the lion.
("tiger" "needs" "lion" "-")
int1
The tiger eats the lion.
("tiger" "eats" "lion" "+")
((triple7 ((triple4) -> (rule4 % int2))) -> (rule8 % int1))
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int1
The lion does not need the lion.
("lion" "needs" "lion" "-")
int2
The lion is round.
("lion" "is" "round" "+")
((((triple7 ((triple4) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int2
The lion does not need the lion.
("lion" "needs" "lion" "-")
int3