The bear is big. The bear is nice. The bear needs the cow. The bear needs the dog. The bear sees the cow. The bear visits the cow. The cow is cold. The cow is red. The dog is big. The dog is nice. The squirrel is big. The squirrel sees the bear. If something needs the dog then it sees the cow. If something is red and it needs the bear then the bear is cold. If something needs the bear and the bear visits the cow then the bear is young. If something needs the dog and the dog needs the bear then it is cold. If something sees the cow then it needs the squirrel. If something sees the cow then the cow visits the squirrel. If something is cold and it needs the bear then it visits the cow. If something is nice and it sees the bear then it is young.
The bear is big.
("bear" "is" "big" "+")
The bear is nice.
("bear" "is" "nice" "+")
The bear needs the cow.
("bear" "needs" "cow" "+")
The bear needs the dog.
("bear" "needs" "dog" "+")
The bear sees the cow.
("bear" "sees" "cow" "+")
The bear visits the cow.
("bear" "visits" "cow" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is red.
("cow" "is" "red" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is nice.
("dog" "is" "nice" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
If something needs the dog then it sees the cow.
((("something" "needs" "dog" "+")) -> ("something" "sees" "cow" "+"))
If something is red and it needs the bear then the bear is cold.
((("something" "is" "red" "+") ("something" "needs" "bear" "+")) -> ("bear" "is" "cold" "+"))
If something needs the bear and the bear visits the cow then the bear is young.
((("something" "needs" "bear" "+") ("bear" "visits" "cow" "+")) -> ("bear" "is" "young" "+"))
If something needs the dog and the dog needs the bear then it is cold.
((("something" "needs" "dog" "+") ("dog" "needs" "bear" "+")) -> ("something" "is" "cold" "+"))
If something sees the cow then it needs the squirrel.
((("something" "sees" "cow" "+")) -> ("something" "needs" "squirrel" "+"))
If something sees the cow then the cow visits the squirrel.
((("something" "sees" "cow" "+")) -> ("cow" "visits" "squirrel" "+"))
If something is cold and it needs the bear then it visits the cow.
((("something" "is" "cold" "+") ("something" "needs" "bear" "+")) -> ("something" "visits" "cow" "+"))
If something is nice and it sees the bear then it is young.
((("something" "is" "nice" "+") ("something" "sees" "bear" "+")) -> ("something" "is" "young" "+"))
The dog is big.
True
1
proof
[(triple9)]
("dog" "is" "big" "+")
triple9
The dog is not big.
False
1
inv-proof
[(triple9)]
("dog" "is" "big" "-")
triple9
The bear needs the squirrel.
True
2
proof
[(((triple5) -> rule5) OR ((((triple4) -> rule1)) -> rule5))]
("bear" "needs" "squirrel" "+")
((triple5) -> (rule5 % int1))
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule5 % int1))
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int1
The bear sees the cow.
("bear" "sees" "cow" "+")
int2
The bear does not need the squirrel.
False
2
inv-proof
[(((triple5) -> rule5) OR ((((triple4) -> rule1)) -> rule5))]
("bear" "needs" "squirrel" "-")
((triple5) -> (rule5 % int1))
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule5 % int1))
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int1
The bear sees the cow.
("bear" "sees" "cow" "+")
int2
The cow is not young.
Unknown
inv-rconc
[@1: The cow is young.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cow" "is" "young" "-")
The dog is young.
Unknown
rconc
[@1: The dog is young.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("dog" "is" "young" "+")
The squirrel does not need the dog.
Unknown
inv-random
[@0: The squirrel needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "dog" "-")
The bear sees the dog.
Unknown
random
[@0: The bear sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "dog" "+")
@0: The bear is big.[(triple1)] The bear is nice.[(triple2)] The bear needs the cow.[(triple3)] The bear needs the dog.[(triple4)] The bear sees the cow.[(triple5 OR ((triple4) -> rule1))] The bear visits the cow.[(triple6)] The cow is cold.[(triple7)] The cow is red.[(triple8)] The dog is big.[(triple9)] The dog is nice.[(triple10)] The squirrel is big.[(triple11)] The squirrel sees the bear.[(triple12)] @1: The bear needs the squirrel.[(((triple5) -> rule5) OR ((((triple4) -> rule1)) -> rule5))] The cow visits the squirrel.[(((triple5) -> rule6) OR ((((triple4) -> rule1)) -> rule6))]
The bear is big.
("bear" "is" "big" "+")
triple1
The bear is nice.
("bear" "is" "nice" "+")
triple2
The bear needs the cow.
("bear" "needs" "cow" "+")
triple3
The bear needs the dog.
("bear" "needs" "dog" "+")
triple4
The bear sees the cow.
("bear" "sees" "cow" "+")
triple5
((triple4) -> (rule1 % int1))
The bear sees the cow.
("bear" "sees" "cow" "+")
int1
The bear visits the cow.
("bear" "visits" "cow" "+")
triple6
The cow is cold.
("cow" "is" "cold" "+")
triple7
The cow is red.
("cow" "is" "red" "+")
triple8
The dog is big.
("dog" "is" "big" "+")
triple9
The dog is nice.
("dog" "is" "nice" "+")
triple10
The squirrel is big.
("squirrel" "is" "big" "+")
triple11
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
triple12
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
((triple5) -> (rule5 % int1))
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule5 % int1))
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int1
The bear sees the cow.
("bear" "sees" "cow" "+")
int2
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
((triple5) -> (rule6 % int1))
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule6 % int1))
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int1
The bear sees the cow.
("bear" "sees" "cow" "+")
int2