The bear is rough. The dog sees the tiger. The squirrel sees the tiger. The tiger needs the squirrel. If the tiger needs the dog and the dog sees the squirrel then the dog needs the tiger. If the bear sees the tiger then the tiger chases the dog. If the squirrel is round and the squirrel chases the tiger then the squirrel is cold. If the bear needs the tiger and the tiger chases the squirrel then the tiger sees the squirrel. If something is round then it needs the dog. All cold things are round. If something is cold then it sees the squirrel. Rough things are cold.
The bear is rough.
("bear" "is" "rough" "+")
The dog sees the tiger.
("dog" "sees" "tiger" "+")
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
If the tiger needs the dog and the dog sees the squirrel then the dog needs the tiger.
((("tiger" "needs" "dog" "+") ("dog" "sees" "squirrel" "+")) -> ("dog" "needs" "tiger" "+"))
If the bear sees the tiger then the tiger chases the dog.
((("bear" "sees" "tiger" "+")) -> ("tiger" "chases" "dog" "+"))
If the squirrel is round and the squirrel chases the tiger then the squirrel is cold.
((("squirrel" "is" "round" "+") ("squirrel" "chases" "tiger" "+")) -> ("squirrel" "is" "cold" "+"))
If the bear needs the tiger and the tiger chases the squirrel then the tiger sees the squirrel.
((("bear" "needs" "tiger" "+") ("tiger" "chases" "squirrel" "+")) -> ("tiger" "sees" "squirrel" "+"))
If something is round then it needs the dog.
((("something" "is" "round" "+")) -> ("something" "needs" "dog" "+"))
All cold things are round.
((("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
If something is cold then it sees the squirrel.
((("something" "is" "cold" "+")) -> ("something" "sees" "squirrel" "+"))
Rough things are cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
The tiger needs the squirrel.
True
1
proof
[(triple4)]
("tiger" "needs" "squirrel" "+")
triple4
The bear is not rough.
False
1
inv-proof
[(triple1)]
("bear" "is" "rough" "-")
triple1
The bear is cold.
True
2
proof
[(((triple1) -> rule8))]
("bear" "is" "cold" "+")
((triple1) -> (rule8 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is not cold.
False
2
inv-proof
[(((triple1) -> rule8))]
("bear" "is" "cold" "-")
((triple1) -> (rule8 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is round.
True
3
proof
[(((((triple1) -> rule8)) -> rule6))]
("bear" "is" "round" "+")
((((triple1) -> (rule8 % int2))) -> (rule6 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear does not see the squirrel.
False
3
inv-proof
[(((((triple1) -> rule8)) -> rule7))]
("bear" "sees" "squirrel" "-")
((((triple1) -> (rule8 % int2))) -> (rule7 % int1))
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear needs the dog.
True
4
proof
[(((((((triple1) -> rule8)) -> rule6)) -> rule5))]
("bear" "needs" "dog" "+")
((((((triple1) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The bear needs the dog.
("bear" "needs" "dog" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The bear is cold.
("bear" "is" "cold" "+")
int3
The bear does not need the dog.
False
4
inv-proof
[(((((((triple1) -> rule8)) -> rule6)) -> rule5))]
("bear" "needs" "dog" "-")
((((((triple1) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The bear needs the dog.
("bear" "needs" "dog" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The bear is cold.
("bear" "is" "cold" "+")
int3
The dog does not need the dog.
Unknown
inv-rconc
[@3: The dog needs the dog.[CWA. Example of deepest failure = (rule5 <- rule6 <- rule8 <- FAIL)]]
("dog" "needs" "dog" "-")
The squirrel is round.
Unknown
rconc
[@2: The squirrel is round.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("squirrel" "is" "round" "+")
The tiger is not cold.
Unknown
inv-rconc
[@1: The tiger is cold.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "is" "cold" "-")
The dog needs the tiger.
Unknown
rconc
[@3: The dog needs the tiger.[CWA. Example of deepest failure = (rule1 <- rule7 <- rule8 <- FAIL)]]
("dog" "needs" "tiger" "+")
The tiger is not red.
Unknown
inv-random
[@0: The tiger is red.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "red" "-")
The dog chases the dog.
Unknown
random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "+")
The tiger is not rough.
Unknown
inv-random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "-")
The dog is blue.
Unknown
random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "+")
@0: The bear is rough.[(triple1)] The dog sees the tiger.[(triple2)] The squirrel sees the tiger.[(triple3)] The tiger needs the squirrel.[(triple4)] @1: The bear is cold.[(((triple1) -> rule8))] @2: The bear is round.[(((((triple1) -> rule8)) -> rule6))] The bear sees the squirrel.[(((((triple1) -> rule8)) -> rule7))] @3: The bear needs the dog.[(((((((triple1) -> rule8)) -> rule6)) -> rule5))]
The bear is rough.
("bear" "is" "rough" "+")
triple1
The dog sees the tiger.
("dog" "sees" "tiger" "+")
triple2
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
triple3
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
triple4
The bear is cold.
("bear" "is" "cold" "+")
((triple1) -> (rule8 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is round.
("bear" "is" "round" "+")
((((triple1) -> (rule8 % int2))) -> (rule6 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
((((triple1) -> (rule8 % int2))) -> (rule7 % int1))
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear needs the dog.
("bear" "needs" "dog" "+")
((((((triple1) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The bear needs the dog.
("bear" "needs" "dog" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The bear is cold.
("bear" "is" "cold" "+")
int3