The bear needs the cow. The cow eats the bear. The cow is green. The cow does not need the bear. The rabbit is green. The tiger is red. The tiger is round. If someone needs the rabbit then the rabbit is round. If the rabbit is kind then the rabbit eats the bear. If the rabbit visits the bear then the rabbit needs the tiger. If someone needs the bear then they do not eat the cow. If someone needs the rabbit and they do not visit the tiger then the tiger needs the rabbit. If someone visits the cow and the cow eats the bear then the cow is not red. If someone is round then they need the rabbit. If someone needs the rabbit then they need the bear.
The bear needs the cow.
("bear" "needs" "cow" "+")
The cow eats the bear.
("cow" "eats" "bear" "+")
The cow is green.
("cow" "is" "green" "+")
The cow does not need the bear.
("cow" "needs" "bear" "-")
The rabbit is green.
("rabbit" "is" "green" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is round.
("tiger" "is" "round" "+")
If someone needs the rabbit then the rabbit is round.
((("someone" "needs" "rabbit" "+")) -> ("rabbit" "is" "round" "+"))
If the rabbit is kind then the rabbit eats the bear.
((("rabbit" "is" "kind" "+")) -> ("rabbit" "eats" "bear" "+"))
If the rabbit visits the bear then the rabbit needs the tiger.
((("rabbit" "visits" "bear" "+")) -> ("rabbit" "needs" "tiger" "+"))
If someone needs the bear then they do not eat the cow.
((("someone" "needs" "bear" "+")) -> ("someone" "eats" "cow" "-"))
If someone needs the rabbit and they do not visit the tiger then the tiger needs the rabbit.
((("someone" "needs" "rabbit" "+") ("someone" "visits" "tiger" "~")) -> ("tiger" "needs" "rabbit" "+"))
If someone visits the cow and the cow eats the bear then the cow is not red.
((("someone" "visits" "cow" "+") ("cow" "eats" "bear" "+")) -> ("cow" "is" "red" "-"))
If someone is round then they need the rabbit.
((("someone" "is" "round" "+")) -> ("someone" "needs" "rabbit" "+"))
If someone needs the rabbit then they need the bear.
((("someone" "needs" "rabbit" "+")) -> ("someone" "needs" "bear" "+"))
The bear needs the cow.
True
1
proof
[(triple1)]
("bear" "needs" "cow" "+")
triple1
The bear does not need the cow.
False
1
inv-proof
[(triple1)]
("bear" "needs" "cow" "-")
triple1
The tiger needs the rabbit.
True
2
proof
[(((triple7) -> rule7))]
("tiger" "needs" "rabbit" "+")
((triple7) -> (rule7 % int1))
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int1
The tiger does not need the rabbit.
False
2
inv-proof
[(((triple7) -> rule7))]
("tiger" "needs" "rabbit" "-")
((triple7) -> (rule7 % int1))
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int1
The rabbit is round.
True
3
proof
[(((((triple7) -> rule7)) -> rule1))]
("rabbit" "is" "round" "+")
((((triple7) -> (rule7 % int2))) -> (rule1 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int2
The tiger does not need the bear.
False
3
inv-proof
[(((((triple7) -> rule7)) -> rule8))]
("tiger" "needs" "bear" "-")
((((triple7) -> (rule7 % int2))) -> (rule8 % int1))
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int1
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int2
The rabbit needs the rabbit.
True
4
proof
[(((((((triple7) -> rule7)) -> rule1)) -> rule7))]
("rabbit" "needs" "rabbit" "+")
((((((triple7) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int3
The tiger eats the cow.
False
4
inv-proof
[(((((((triple7) -> rule7)) -> rule8)) -> rule4))]
("tiger" "eats" "cow" "+")
((((((triple7) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The tiger does not eat the cow.
("tiger" "eats" "cow" "-")
int1
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int2
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int3
The rabbit needs the bear.
True
5
proof
[(((((((((triple7) -> rule7)) -> rule1)) -> rule7)) -> rule8))]
("rabbit" "needs" "bear" "+")
((((((((triple7) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int4
The rabbit does not need the bear.
False
5
inv-proof
[(((((((((triple7) -> rule7)) -> rule1)) -> rule7)) -> rule8))]
("rabbit" "needs" "bear" "-")
((((((((triple7) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int4
The rabbit does not eat the cow.
True
6
proof
[(((((((((((triple7) -> rule7)) -> rule1)) -> rule7)) -> rule8)) -> rule4))]
("rabbit" "eats" "cow" "-")
((((((((((triple7) -> (rule7 % int5))) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The rabbit does not eat the cow.
("rabbit" "eats" "cow" "-")
int1
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
int2
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int3
The rabbit is round.
("rabbit" "is" "round" "+")
int4
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int5
The rabbit eats the cow.
False
6
inv-proof
[(((((((((((triple7) -> rule7)) -> rule1)) -> rule7)) -> rule8)) -> rule4))]
("rabbit" "eats" "cow" "+")
((((((((((triple7) -> (rule7 % int5))) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The rabbit does not eat the cow.
("rabbit" "eats" "cow" "-")
int1
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
int2
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int3
The rabbit is round.
("rabbit" "is" "round" "+")
int4
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int5
The rabbit does not need the tiger.
Unknown
inv-rconc
[@1: The rabbit needs the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "needs" "tiger" "-")
The rabbit eats the bear.
Unknown
rconc
[@1: The rabbit eats the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "eats" "bear" "+")
The bear does not need the bear.
Unknown
inv-rconc
[@2: The bear needs the bear.[CWA. Example of deepest failure = (rule8 <- rule7 <- FAIL)]]
("bear" "needs" "bear" "-")
The cow needs the rabbit.
Unknown
rconc
[@1: The cow needs the rabbit.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cow" "needs" "rabbit" "+")
The bear does not need the rabbit.
Unknown
inv-rconc
[@1: The bear needs the rabbit.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bear" "needs" "rabbit" "-")
The bear eats the bear.
Unknown
random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "+")
The bear does not need the tiger.
Unknown
inv-random
[@0: The bear needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "tiger" "-")
The rabbit visits the cow.
Unknown
random
[@0: The rabbit visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "cow" "+")
The bear does not visit the tiger.
Unknown
inv-random
[@0: The bear visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "tiger" "-")
The tiger is kind.
Unknown
random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "+")
The bear is not red.
Unknown
inv-random
[@0: The bear is red.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "red" "-")
The cow is round.
Unknown
random
[@0: The cow is round.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "round" "+")
@0: The bear needs the cow.[(triple1)] The cow does not need the bear.[(triple4)] The cow eats the bear.[(triple2)] The cow is green.[(triple3)] The rabbit is green.[(triple5)] The tiger is red.[(triple6)] The tiger is round.[(triple7)] @1: The tiger needs the rabbit.[(((triple7) -> rule7))] @2: The rabbit is round.[(((((triple7) -> rule7)) -> rule1))] The tiger needs the bear.[(((((triple7) -> rule7)) -> rule8))] @3: The rabbit needs the rabbit.[(((((((triple7) -> rule7)) -> rule1)) -> rule7))] The tiger does not eat the cow.[(((((((triple7) -> rule7)) -> rule8)) -> rule4))] @4: The rabbit needs the bear.[(((((((((triple7) -> rule7)) -> rule1)) -> rule7)) -> rule8))] @5: The rabbit does not eat the cow.[(((((((((((triple7) -> rule7)) -> rule1)) -> rule7)) -> rule8)) -> rule4))]
The bear needs the cow.
("bear" "needs" "cow" "+")
triple1
The cow does not need the bear.
("cow" "needs" "bear" "-")
triple4
The cow eats the bear.
("cow" "eats" "bear" "+")
triple2
The cow is green.
("cow" "is" "green" "+")
triple3
The rabbit is green.
("rabbit" "is" "green" "+")
triple5
The tiger is red.
("tiger" "is" "red" "+")
triple6
The tiger is round.
("tiger" "is" "round" "+")
triple7
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
((triple7) -> (rule7 % int1))
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
((((triple7) -> (rule7 % int2))) -> (rule1 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int2
The tiger needs the bear.
("tiger" "needs" "bear" "+")
((((triple7) -> (rule7 % int2))) -> (rule8 % int1))
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int1
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int2
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((((((triple7) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int3
The tiger does not eat the cow.
("tiger" "eats" "cow" "-")
((((((triple7) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The tiger does not eat the cow.
("tiger" "eats" "cow" "-")
int1
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int2
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int3
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
((((((((triple7) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int4
The rabbit does not eat the cow.
("rabbit" "eats" "cow" "-")
((((((((((triple7) -> (rule7 % int5))) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The rabbit does not eat the cow.
("rabbit" "eats" "cow" "-")
int1
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
int2
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int3
The rabbit is round.
("rabbit" "is" "round" "+")
int4
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int5