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