The bear eats the squirrel. The bear eats the tiger. The bear does not visit the cat. The bear does not visit the squirrel. The cat chases the bear. The cat does not chase the squirrel. The cat chases the tiger. The cat eats the bear. The cat visits the bear. The squirrel chases the bear. The squirrel eats the cat. The squirrel is not round. The squirrel visits the bear. The tiger chases the cat. The tiger eats the cat. The tiger does not visit the bear. All blue people are round. If someone chases the tiger then they are round. If someone chases the bear then the bear is blue. If someone is round then they eat the bear. If someone eats the bear then they are cold. If someone chases the bear and the bear is cold then they do not chase the cat. If someone eats the squirrel and the squirrel is not kind then the squirrel chases the bear.
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
The bear eats the tiger.
("bear" "eats" "tiger" "+")
The bear does not visit the cat.
("bear" "visits" "cat" "-")
The bear does not visit the squirrel.
("bear" "visits" "squirrel" "-")
The cat chases the bear.
("cat" "chases" "bear" "+")
The cat does not chase the squirrel.
("cat" "chases" "squirrel" "-")
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The cat eats the bear.
("cat" "eats" "bear" "+")
The cat visits the bear.
("cat" "visits" "bear" "+")
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
The squirrel is not round.
("squirrel" "is" "round" "-")
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
The tiger chases the cat.
("tiger" "chases" "cat" "+")
The tiger eats the cat.
("tiger" "eats" "cat" "+")
The tiger does not visit the bear.
("tiger" "visits" "bear" "-")
All blue people are round.
((("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
If someone chases the tiger then they are round.
((("someone" "chases" "tiger" "+")) -> ("someone" "is" "round" "+"))
If someone chases the bear then the bear is blue.
((("someone" "chases" "bear" "+")) -> ("bear" "is" "blue" "+"))
If someone is round then they eat the bear.
((("someone" "is" "round" "+")) -> ("someone" "eats" "bear" "+"))
If someone eats the bear then they are cold.
((("someone" "eats" "bear" "+")) -> ("someone" "is" "cold" "+"))
If someone chases the bear and the bear is cold then they do not chase the cat.
((("someone" "chases" "bear" "+") ("bear" "is" "cold" "+")) -> ("someone" "chases" "cat" "-"))
If someone eats the squirrel and the squirrel is not kind then the squirrel chases the bear.
((("someone" "eats" "squirrel" "+") ("squirrel" "is" "kind" "~")) -> ("squirrel" "chases" "bear" "+"))
The bear does not visit the cat.
True
1
proof
[(triple3)]
("bear" "visits" "cat" "-")
triple3
The cat does not chase the bear.
False
1
inv-proof
[(triple5)]
("cat" "chases" "bear" "-")
triple5
The cat is round.
True
2
proof
[(((triple7) -> rule2))]
("cat" "is" "round" "+")
((triple7) -> (rule2 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The bear is not blue.
False
2
inv-proof
[(((triple10) -> rule3) OR ((triple5) -> rule3))]
("bear" "is" "blue" "-")
((triple10) -> (rule3 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
((triple5) -> (rule3 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The bear is round.
True
3
proof
[(((((triple10) -> rule3)) -> rule1) OR ((((triple5) -> rule3)) -> rule1))]
("bear" "is" "round" "+")
((((triple10) -> (rule3 % int2))) -> (rule1 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
((((triple5) -> (rule3 % int2))) -> (rule1 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
The bear is not round.
False
3
inv-proof
[(((((triple10) -> rule3)) -> rule1) OR ((((triple5) -> rule3)) -> rule1))]
("bear" "is" "round" "-")
((((triple10) -> (rule3 % int2))) -> (rule1 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
((((triple5) -> (rule3 % int2))) -> (rule1 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
The bear eats the bear.
True
4
proof
[(((((((triple10) -> rule3)) -> rule1)) -> rule4) OR ((((((triple5) -> rule3)) -> rule1)) -> rule4))]
("bear" "eats" "bear" "+")
((((((triple10) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
int3
((((((triple5) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
int3
The bear does not eat the bear.
False
4
inv-proof
[(((((((triple10) -> rule3)) -> rule1)) -> rule4) OR ((((((triple5) -> rule3)) -> rule1)) -> rule4))]
("bear" "eats" "bear" "-")
((((((triple10) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
int3
((((((triple5) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
int3
The bear is cold.
True
5
proof
[(((((((((triple10) -> rule3)) -> rule1)) -> rule4)) -> rule5) OR ((((((((triple5) -> rule3)) -> rule1)) -> rule4)) -> rule5))]
("bear" "is" "cold" "+")
((((((((triple10) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear eats the bear.
("bear" "eats" "bear" "+")
int2
The bear is round.
("bear" "is" "round" "+")
int3
The bear is blue.
("bear" "is" "blue" "+")
int4
((((((((triple5) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear eats the bear.
("bear" "eats" "bear" "+")
int2
The bear is round.
("bear" "is" "round" "+")
int3
The bear is blue.
("bear" "is" "blue" "+")
int4
The bear is not cold.
False
5
inv-proof
[(((((((((triple10) -> rule3)) -> rule1)) -> rule4)) -> rule5) OR ((((((((triple5) -> rule3)) -> rule1)) -> rule4)) -> rule5))]
("bear" "is" "cold" "-")
((((((((triple10) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear eats the bear.
("bear" "eats" "bear" "+")
int2
The bear is round.
("bear" "is" "round" "+")
int3
The bear is blue.
("bear" "is" "blue" "+")
int4
((((((((triple5) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear eats the bear.
("bear" "eats" "bear" "+")
int2
The bear is round.
("bear" "is" "round" "+")
int3
The bear is blue.
("bear" "is" "blue" "+")
int4
The squirrel does not chase the cat.
True
7
proof
[(((triple10 ((((((((triple10) -> rule3)) -> rule1)) -> rule4)) -> rule5)) -> rule6) OR ((triple10 ((((((((triple5) -> rule3)) -> rule1)) -> rule4)) -> rule5)) -> rule6))]
("squirrel" "chases" "cat" "-")
((triple10 ((((((((triple10) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The squirrel does not chase the cat.
("squirrel" "chases" "cat" "-")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear eats the bear.
("bear" "eats" "bear" "+")
int3
The bear is round.
("bear" "is" "round" "+")
int4
The bear is blue.
("bear" "is" "blue" "+")
int5
((triple10 ((((((((triple5) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The squirrel does not chase the cat.
("squirrel" "chases" "cat" "-")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear eats the bear.
("bear" "eats" "bear" "+")
int3
The bear is round.
("bear" "is" "round" "+")
int4
The bear is blue.
("bear" "is" "blue" "+")
int5
The squirrel chases the cat.
False
7
inv-proof
[(((triple10 ((((((((triple10) -> rule3)) -> rule1)) -> rule4)) -> rule5)) -> rule6) OR ((triple10 ((((((((triple5) -> rule3)) -> rule1)) -> rule4)) -> rule5)) -> rule6))]
("squirrel" "chases" "cat" "+")
((triple10 ((((((((triple10) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The squirrel does not chase the cat.
("squirrel" "chases" "cat" "-")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear eats the bear.
("bear" "eats" "bear" "+")
int3
The bear is round.
("bear" "is" "round" "+")
int4
The bear is blue.
("bear" "is" "blue" "+")
int5
((triple10 ((((((((triple5) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The squirrel does not chase the cat.
("squirrel" "chases" "cat" "-")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear eats the bear.
("bear" "eats" "bear" "+")
int3
The bear is round.
("bear" "is" "round" "+")
int4
The bear is blue.
("bear" "is" "blue" "+")
int5
The squirrel does not eat the bear.
Unknown
inv-rconc
[@1: The squirrel eats the bear.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "eats" "bear" "-")
The tiger is round.
Unknown
rconc
[@1: The tiger is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "is" "round" "+")
The tiger is not cold.
Unknown
inv-rconc
[@3: The tiger is cold.[CWA. Example of deepest failure = (rule5 <- rule4 <- rule1 <- FAIL)]]
("tiger" "is" "cold" "-")
The tiger eats the bear.
Unknown
rconc
[@2: The tiger eats the bear.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("tiger" "eats" "bear" "+")
The squirrel is not cold.
Unknown
inv-rconc
[@2: The squirrel is cold.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("squirrel" "is" "cold" "-")
The cat visits the tiger.
Unknown
random
[@0: The cat visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "tiger" "+")
The cat does not visit the squirrel.
Unknown
inv-random
[@0: The cat visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "squirrel" "-")
The squirrel eats the squirrel.
Unknown
random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "+")
The squirrel does not chase the tiger.
Unknown
inv-random
[@0: The squirrel chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "tiger" "-")
The squirrel visits the tiger.
Unknown
random
[@0: The squirrel visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "tiger" "+")
The tiger is not big.
Unknown
inv-random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "-")
The bear is big.
Unknown
random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "+")
@0: The bear does not visit the cat.[(triple3)] The bear does not visit the squirrel.[(triple4)] The bear eats the squirrel.[(triple1)] The bear eats the tiger.[(triple2)] The cat chases the bear.[(triple5)] The cat chases the tiger.[(triple7)] The cat does not chase the squirrel.[(triple6)] The cat eats the bear.[(triple8 OR ((((triple7) -> rule2)) -> rule4))] The cat visits the bear.[(triple9)] The squirrel chases the bear.[(triple10)] The squirrel eats the cat.[(triple11)] The squirrel is not round.[(triple12)] The squirrel visits the bear.[(triple13)] The tiger chases the cat.[(triple14)] The tiger does not visit the bear.[(triple16)] The tiger eats the cat.[(triple15)] @1: The bear is blue.[(((triple10) -> rule3) OR ((triple5) -> rule3))] The cat is cold.[(((triple8) -> rule5) OR ((((((triple7) -> rule2)) -> rule4)) -> rule5))] The cat is round.[(((triple7) -> rule2))] @2: The bear is round.[(((((triple10) -> rule3)) -> rule1) OR ((((triple5) -> rule3)) -> rule1))] @3: The bear eats the bear.[(((((((triple10) -> rule3)) -> rule1)) -> rule4) OR ((((((triple5) -> rule3)) -> rule1)) -> rule4))] @4: The bear is cold.[(((((((((triple10) -> rule3)) -> rule1)) -> rule4)) -> rule5) OR ((((((((triple5) -> rule3)) -> rule1)) -> rule4)) -> rule5))] @5: The cat does not chase the cat.[(((triple5 ((((((((triple10) -> rule3)) -> rule1)) -> rule4)) -> rule5)) -> rule6) OR ((triple5 ((((((((triple5) -> rule3)) -> rule1)) -> rule4)) -> rule5)) -> rule6))] The squirrel does not chase the cat.[(((triple10 ((((((((triple10) -> rule3)) -> rule1)) -> rule4)) -> rule5)) -> rule6) OR ((triple10 ((((((((triple5) -> rule3)) -> rule1)) -> rule4)) -> rule5)) -> rule6))]
The bear does not visit the cat.
("bear" "visits" "cat" "-")
triple3
The bear does not visit the squirrel.
("bear" "visits" "squirrel" "-")
triple4
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
triple1
The bear eats the tiger.
("bear" "eats" "tiger" "+")
triple2
The cat chases the bear.
("cat" "chases" "bear" "+")
triple5
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple7
The cat does not chase the squirrel.
("cat" "chases" "squirrel" "-")
triple6
The cat eats the bear.
("cat" "eats" "bear" "+")
triple8
((((triple7) -> (rule2 % int2))) -> (rule4 % int1))
The cat eats the bear.
("cat" "eats" "bear" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat visits the bear.
("cat" "visits" "bear" "+")
triple9
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
triple10
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
triple11
The squirrel is not round.
("squirrel" "is" "round" "-")
triple12
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
triple13
The tiger chases the cat.
("tiger" "chases" "cat" "+")
triple14
The tiger does not visit the bear.
("tiger" "visits" "bear" "-")
triple16
The tiger eats the cat.
("tiger" "eats" "cat" "+")
triple15
The bear is blue.
("bear" "is" "blue" "+")
((triple10) -> (rule3 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
((triple5) -> (rule3 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
((triple8) -> (rule5 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
((((((triple7) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat eats the bear.
("cat" "eats" "bear" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The cat is round.
("cat" "is" "round" "+")
((triple7) -> (rule2 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The bear is round.
("bear" "is" "round" "+")
((((triple10) -> (rule3 % int2))) -> (rule1 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
((((triple5) -> (rule3 % int2))) -> (rule1 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
The bear eats the bear.
("bear" "eats" "bear" "+")
((((((triple10) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
int3
((((((triple5) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
int3
The bear is cold.
("bear" "is" "cold" "+")
((((((((triple10) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear eats the bear.
("bear" "eats" "bear" "+")
int2
The bear is round.
("bear" "is" "round" "+")
int3
The bear is blue.
("bear" "is" "blue" "+")
int4
((((((((triple5) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear eats the bear.
("bear" "eats" "bear" "+")
int2
The bear is round.
("bear" "is" "round" "+")
int3
The bear is blue.
("bear" "is" "blue" "+")
int4
The cat does not chase the cat.
("cat" "chases" "cat" "-")
((triple5 ((((((((triple10) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The cat does not chase the cat.
("cat" "chases" "cat" "-")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear eats the bear.
("bear" "eats" "bear" "+")
int3
The bear is round.
("bear" "is" "round" "+")
int4
The bear is blue.
("bear" "is" "blue" "+")
int5
((triple5 ((((((((triple5) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The cat does not chase the cat.
("cat" "chases" "cat" "-")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear eats the bear.
("bear" "eats" "bear" "+")
int3
The bear is round.
("bear" "is" "round" "+")
int4
The bear is blue.
("bear" "is" "blue" "+")
int5
The squirrel does not chase the cat.
("squirrel" "chases" "cat" "-")
((triple10 ((((((((triple10) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The squirrel does not chase the cat.
("squirrel" "chases" "cat" "-")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear eats the bear.
("bear" "eats" "bear" "+")
int3
The bear is round.
("bear" "is" "round" "+")
int4
The bear is blue.
("bear" "is" "blue" "+")
int5
((triple10 ((((((((triple5) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The squirrel does not chase the cat.
("squirrel" "chases" "cat" "-")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear eats the bear.
("bear" "eats" "bear" "+")
int3
The bear is round.
("bear" "is" "round" "+")
int4
The bear is blue.
("bear" "is" "blue" "+")
int5