The bear is rough. The bear needs the cow. The cow visits the bear. The cow visits the dog. The dog is young. The dog visits the cow. The squirrel eats the bear. If something is cold then it does not visit the bear. If something visits the dog then it needs the squirrel. If something is cold then it needs the squirrel. If something eats the dog then the dog eats the squirrel. If something needs the bear and the bear does not eat the dog then the dog needs the squirrel. If the squirrel is rough and the squirrel visits the cow then the squirrel eats the bear. If something needs the squirrel then the squirrel is cold. If the squirrel is cold and the squirrel visits the cow then the squirrel does not need the bear. If something needs the squirrel then it visits the cow.
The bear is rough.
("bear" "is" "rough" "+")
The bear needs the cow.
("bear" "needs" "cow" "+")
The cow visits the bear.
("cow" "visits" "bear" "+")
The cow visits the dog.
("cow" "visits" "dog" "+")
The dog is young.
("dog" "is" "young" "+")
The dog visits the cow.
("dog" "visits" "cow" "+")
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
If something is cold then it does not visit the bear.
((("something" "is" "cold" "+")) -> ("something" "visits" "bear" "-"))
If something visits the dog then it needs the squirrel.
((("something" "visits" "dog" "+")) -> ("something" "needs" "squirrel" "+"))
If something is cold then it needs the squirrel.
((("something" "is" "cold" "+")) -> ("something" "needs" "squirrel" "+"))
If something eats the dog then the dog eats the squirrel.
((("something" "eats" "dog" "+")) -> ("dog" "eats" "squirrel" "+"))
If something needs the bear and the bear does not eat the dog then the dog needs the squirrel.
((("something" "needs" "bear" "+") ("bear" "eats" "dog" "~")) -> ("dog" "needs" "squirrel" "+"))
If the squirrel is rough and the squirrel visits the cow then the squirrel eats the bear.
((("squirrel" "is" "rough" "+") ("squirrel" "visits" "cow" "+")) -> ("squirrel" "eats" "bear" "+"))
If something needs the squirrel then the squirrel is cold.
((("something" "needs" "squirrel" "+")) -> ("squirrel" "is" "cold" "+"))
If the squirrel is cold and the squirrel visits the cow then the squirrel does not need the bear.
((("squirrel" "is" "cold" "+") ("squirrel" "visits" "cow" "+")) -> ("squirrel" "needs" "bear" "-"))
If something needs the squirrel then it visits the cow.
((("something" "needs" "squirrel" "+")) -> ("something" "visits" "cow" "+"))
The dog visits the cow.
True
1
proof
[(triple6)]
("dog" "visits" "cow" "+")
triple6
The squirrel does not eat the bear.
False
1
inv-proof
[(triple7)]
("squirrel" "eats" "bear" "-")
triple7
The cow needs the squirrel.
True
2
proof
[(((triple4) -> rule2))]
("cow" "needs" "squirrel" "+")
((triple4) -> (rule2 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
The cow does not need the squirrel.
False
2
inv-proof
[(((triple4) -> rule2))]
("cow" "needs" "squirrel" "-")
((triple4) -> (rule2 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
The cow visits the cow.
True
3
proof
[(((((triple4) -> rule2)) -> rule9))]
("cow" "visits" "cow" "+")
((((triple4) -> (rule2 % int2))) -> (rule9 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int2
The squirrel is not cold.
False
3
inv-proof
[(((((triple4) -> rule2)) -> rule7))]
("squirrel" "is" "cold" "-")
((((triple4) -> (rule2 % int2))) -> (rule7 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int2
The squirrel needs the squirrel.
True
4
proof
[(((((((triple4) -> rule2)) -> rule7)) -> rule3))]
("squirrel" "needs" "squirrel" "+")
((((((triple4) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int3
The squirrel visits the bear.
False
4
inv-proof
[(((((((triple4) -> rule2)) -> rule7)) -> rule1))]
("squirrel" "visits" "bear" "+")
((((((triple4) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The squirrel does not visit the bear.
("squirrel" "visits" "bear" "-")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int3
The squirrel visits the cow.
True
5
proof
[(((((((((triple4) -> rule2)) -> rule7)) -> rule3)) -> rule9))]
("squirrel" "visits" "cow" "+")
((((((((triple4) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule9 % int1))
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int1
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int4
The squirrel does not visit the cow.
False
5
inv-proof
[(((((((((triple4) -> rule2)) -> rule7)) -> rule3)) -> rule9))]
("squirrel" "visits" "cow" "-")
((((((((triple4) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule9 % int1))
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int1
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int4
The squirrel does not need the bear.
True
9
proof
[(((((((triple4) -> rule2)) -> rule7) ((((((((triple4) -> rule2)) -> rule7)) -> rule3)) -> rule9)) -> rule8))]
("squirrel" "needs" "bear" "-")
((((((triple4) -> (rule2 % int5))) -> (rule7 % int4)) ((((((((triple4) -> (rule2 % int5))) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule9 % int2))) -> (rule8 % int1))
The squirrel does not need the bear.
("squirrel" "needs" "bear" "-")
int1
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int2
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int3
The squirrel is cold.
("squirrel" "is" "cold" "+")
int4
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int5
The squirrel needs the bear.
False
9
inv-proof
[(((((((triple4) -> rule2)) -> rule7) ((((((((triple4) -> rule2)) -> rule7)) -> rule3)) -> rule9)) -> rule8))]
("squirrel" "needs" "bear" "+")
((((((triple4) -> (rule2 % int5))) -> (rule7 % int4)) ((((((((triple4) -> (rule2 % int5))) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule9 % int2))) -> (rule8 % int1))
The squirrel does not need the bear.
("squirrel" "needs" "bear" "-")
int1
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int2
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int3
The squirrel is cold.
("squirrel" "is" "cold" "+")
int4
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int5
The dog does not eat the squirrel.
Unknown
inv-rconc
[@1: The dog eats the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "eats" "squirrel" "-")
The dog needs the squirrel.
Unknown
rconc
[@1: The dog needs the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "needs" "squirrel" "+")
The bear does not need the squirrel.
Unknown
inv-rconc
[@1: The bear needs the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "needs" "squirrel" "-")
The bear visits the cow.
Unknown
rconc
[@2: The bear visits the cow.[CWA. Example of deepest failure = (rule9 <- rule2 <- FAIL)]]
("bear" "visits" "cow" "+")
The bear does not eat the cow.
Unknown
inv-random
[@0: The bear eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "cow" "-")
The bear visits the dog.
Unknown
random
[@0: The bear visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "dog" "+")
The bear is not kind.
Unknown
inv-random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "-")
The dog is cold.
Unknown
random
[@0: The dog is cold.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "cold" "+")
The squirrel does not visit the dog.
Unknown
inv-random
[@0: The squirrel visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "dog" "-")
The bear needs the dog.
Unknown
random
[@0: The bear needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "dog" "+")
The squirrel does not visit the squirrel.
Unknown
inv-random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "-")
The dog visits the dog.
Unknown
random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "+")
@0: The bear is rough.[(triple1)] The bear needs the cow.[(triple2)] The cow visits the bear.[(triple3)] The cow visits the dog.[(triple4)] The dog is young.[(triple5)] The dog visits the cow.[(triple6)] The squirrel eats the bear.[(triple7)] @1: The cow needs the squirrel.[(((triple4) -> rule2))] @2: The cow visits the cow.[(((((triple4) -> rule2)) -> rule9))] The squirrel is cold.[(((((triple4) -> rule2)) -> rule7))] @3: The squirrel does not visit the bear.[(((((((triple4) -> rule2)) -> rule7)) -> rule1))] The squirrel needs the squirrel.[(((((((triple4) -> rule2)) -> rule7)) -> rule3))] @4: The squirrel visits the cow.[(((((((((triple4) -> rule2)) -> rule7)) -> rule3)) -> rule9))] @5: The squirrel does not need the bear.[(((((((triple4) -> rule2)) -> rule7) ((((((((triple4) -> rule2)) -> rule7)) -> rule3)) -> rule9)) -> rule8))]
The bear is rough.
("bear" "is" "rough" "+")
triple1
The bear needs the cow.
("bear" "needs" "cow" "+")
triple2
The cow visits the bear.
("cow" "visits" "bear" "+")
triple3
The cow visits the dog.
("cow" "visits" "dog" "+")
triple4
The dog is young.
("dog" "is" "young" "+")
triple5
The dog visits the cow.
("dog" "visits" "cow" "+")
triple6
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
triple7
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
((triple4) -> (rule2 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
((((triple4) -> (rule2 % int2))) -> (rule9 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
((((triple4) -> (rule2 % int2))) -> (rule7 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int2
The squirrel does not visit the bear.
("squirrel" "visits" "bear" "-")
((((((triple4) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The squirrel does not visit the bear.
("squirrel" "visits" "bear" "-")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int3
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
((((((triple4) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int3
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
((((((((triple4) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule9 % int1))
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int1
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int4
The squirrel does not need the bear.
("squirrel" "needs" "bear" "-")
((((((triple4) -> (rule2 % int5))) -> (rule7 % int4)) ((((((((triple4) -> (rule2 % int5))) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule9 % int2))) -> (rule8 % int1))
The squirrel does not need the bear.
("squirrel" "needs" "bear" "-")
int1
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int2
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int3
The squirrel is cold.
("squirrel" "is" "cold" "+")
int4
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int5