The cow eats the tiger. The lion does not need the cow. The tiger is young. If something sees the lion then it needs the cow. If something eats the lion then the lion is kind. If something eats the cow and the cow sees the lion then the cow is not kind. If something needs the cow then the cow eats the lion. If something eats the tiger then the tiger sees the lion. If something needs the cow then it does not see the cow. If something eats the lion then the lion is red. If the lion is not red and the lion does not eat the cow then the lion sees the cow.
The cow eats the tiger.
("cow" "eats" "tiger" "+")
The lion does not need the cow.
("lion" "needs" "cow" "-")
The tiger is young.
("tiger" "is" "young" "+")
If something sees the lion then it needs the cow.
((("something" "sees" "lion" "+")) -> ("something" "needs" "cow" "+"))
If something eats the lion then the lion is kind.
((("something" "eats" "lion" "+")) -> ("lion" "is" "kind" "+"))
If something eats the cow and the cow sees the lion then the cow is not kind.
((("something" "eats" "cow" "+") ("cow" "sees" "lion" "+")) -> ("cow" "is" "kind" "-"))
If something needs the cow then the cow eats the lion.
((("something" "needs" "cow" "+")) -> ("cow" "eats" "lion" "+"))
If something eats the tiger then the tiger sees the lion.
((("something" "eats" "tiger" "+")) -> ("tiger" "sees" "lion" "+"))
If something needs the cow then it does not see the cow.
((("something" "needs" "cow" "+")) -> ("something" "sees" "cow" "-"))
If something eats the lion then the lion is red.
((("something" "eats" "lion" "+")) -> ("lion" "is" "red" "+"))
If the lion is not red and the lion does not eat the cow then the lion sees the cow.
((("lion" "is" "red" "~") ("lion" "eats" "cow" "~")) -> ("lion" "sees" "cow" "+"))
The lion does not need the cow.
True
1
proof
[(triple2)]
("lion" "needs" "cow" "-")
triple2
The lion needs the cow.
False
1
inv-proof
[(triple2)]
("lion" "needs" "cow" "+")
triple2
The tiger sees the lion.
True
2
proof
[(((triple1) -> rule5))]
("tiger" "sees" "lion" "+")
((triple1) -> (rule5 % int1))
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int1
The tiger does not see the lion.
False
2
inv-proof
[(((triple1) -> rule5))]
("tiger" "sees" "lion" "-")
((triple1) -> (rule5 % int1))
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int1
The tiger needs the cow.
True
3
proof
[(((((triple1) -> rule5)) -> rule1))]
("tiger" "needs" "cow" "+")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int2
The tiger does not need the cow.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule1))]
("tiger" "needs" "cow" "-")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int2
The cow eats the lion.
True
4
proof
[(((((((triple1) -> rule5)) -> rule1)) -> rule4))]
("cow" "eats" "lion" "+")
((((((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The cow eats the lion.
("cow" "eats" "lion" "+")
int1
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int2
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int3
The tiger sees the cow.
False
4
inv-proof
[(((((((triple1) -> rule5)) -> rule1)) -> rule6))]
("tiger" "sees" "cow" "+")
((((((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The tiger does not see the cow.
("tiger" "sees" "cow" "-")
int1
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int2
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int3
The cow does not need the cow.
Unknown
inv-rconc
[@1: The cow needs the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "needs" "cow" "-")
The lion sees the cow.
Unknown
rconc
[@1: The lion sees the cow.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("lion" "sees" "cow" "+")
The tiger does not eat the cow.
Unknown
inv-random
[@0: The tiger eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "cow" "-")
The tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
The tiger is not round.
Unknown
inv-random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "-")
The cow eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
The tiger does not eat the tiger.
Unknown
inv-random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "-")
The tiger is red.
Unknown
random
[@0: The tiger is red.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "red" "+")
@0: The cow eats the tiger.[(triple1)] The lion does not need the cow.[(triple2)] The tiger is young.[(triple3)] @1: The tiger sees the lion.[(((triple1) -> rule5))] @2: The tiger needs the cow.[(((((triple1) -> rule5)) -> rule1))] @3: The cow eats the lion.[(((((((triple1) -> rule5)) -> rule1)) -> rule4))] The tiger does not see the cow.[(((((((triple1) -> rule5)) -> rule1)) -> rule6))] @4: The lion is kind.[(((((((((triple1) -> rule5)) -> rule1)) -> rule4)) -> rule2))] The lion is red.[(((((((((triple1) -> rule5)) -> rule1)) -> rule4)) -> rule7))]
The cow eats the tiger.
("cow" "eats" "tiger" "+")
triple1
The lion does not need the cow.
("lion" "needs" "cow" "-")
triple2
The tiger is young.
("tiger" "is" "young" "+")
triple3
The tiger sees the lion.
("tiger" "sees" "lion" "+")
((triple1) -> (rule5 % int1))
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int1
The tiger needs the cow.
("tiger" "needs" "cow" "+")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int2
The cow eats the lion.
("cow" "eats" "lion" "+")
((((((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The cow eats the lion.
("cow" "eats" "lion" "+")
int1
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int2
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int3
The tiger does not see the cow.
("tiger" "sees" "cow" "-")
((((((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The tiger does not see the cow.
("tiger" "sees" "cow" "-")
int1
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int2
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int3
The lion is kind.
("lion" "is" "kind" "+")
((((((((triple1) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The cow eats the lion.
("cow" "eats" "lion" "+")
int2
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int3
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int4
The lion is red.
("lion" "is" "red" "+")
((((((((triple1) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The cow eats the lion.
("cow" "eats" "lion" "+")
int2
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int3
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int4