The bear eats the squirrel. The bear likes the squirrel. The bear visits the tiger. The squirrel eats the bear. The squirrel is green. The squirrel is nice. The squirrel likes the bear. The squirrel likes the tiger. The squirrel visits the bear. The tiger eats the bear. The tiger is green. The tiger is nice. The tiger likes the bear. The tiger does not like the squirrel. The tiger visits the bear. The tiger does not visit the squirrel. If something eats the tiger and it visits the tiger then it does not visit the bear. If something likes the tiger and the tiger eats the bear then it likes the bear. If something visits the squirrel and it eats the bear then the squirrel likes the tiger. If something is round then it likes the tiger. If something eats the squirrel then it eats the tiger. If something visits the bear then the bear eats the tiger. If the squirrel likes the tiger and the squirrel eats the tiger then the squirrel does not eat the bear. If the tiger does not like the bear then the bear is not kind.
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
The bear visits the tiger.
("bear" "visits" "tiger" "+")
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
The tiger eats the bear.
("tiger" "eats" "bear" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger likes the bear.
("tiger" "likes" "bear" "+")
The tiger does not like the squirrel.
("tiger" "likes" "squirrel" "-")
The tiger visits the bear.
("tiger" "visits" "bear" "+")
The tiger does not visit the squirrel.
("tiger" "visits" "squirrel" "-")
If something eats the tiger and it visits the tiger then it does not visit the bear.
((("something" "eats" "tiger" "+") ("something" "visits" "tiger" "+")) -> ("something" "visits" "bear" "-"))
If something likes the tiger and the tiger eats the bear then it likes the bear.
((("something" "likes" "tiger" "+") ("tiger" "eats" "bear" "+")) -> ("something" "likes" "bear" "+"))
If something visits the squirrel and it eats the bear then the squirrel likes the tiger.
((("something" "visits" "squirrel" "+") ("something" "eats" "bear" "+")) -> ("squirrel" "likes" "tiger" "+"))
If something is round then it likes the tiger.
((("something" "is" "round" "+")) -> ("something" "likes" "tiger" "+"))
If something eats the squirrel then it eats the tiger.
((("something" "eats" "squirrel" "+")) -> ("something" "eats" "tiger" "+"))
If something visits the bear then the bear eats the tiger.
((("something" "visits" "bear" "+")) -> ("bear" "eats" "tiger" "+"))
If the squirrel likes the tiger and the squirrel eats the tiger then the squirrel does not eat the bear.
((("squirrel" "likes" "tiger" "+") ("squirrel" "eats" "tiger" "+")) -> ("squirrel" "eats" "bear" "-"))
If the tiger does not like the bear then the bear is not kind.
((("tiger" "likes" "bear" "~")) -> ("bear" "is" "kind" "-"))
The tiger is nice.
True
1
proof
[(triple12)]
("tiger" "is" "nice" "+")
triple12
The squirrel does not visit the bear.
False
1
inv-proof
[(triple9)]
("squirrel" "visits" "bear" "-")
triple9
The bear eats the tiger.
True
2
proof
[(((triple1) -> rule5) OR ((triple15) -> rule6) OR ((triple9) -> rule6))]
("bear" "eats" "tiger" "+")
((triple1) -> (rule5 % int1))
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int1
((triple15) -> (rule6 % int1))
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int1
((triple9) -> (rule6 % int1))
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int1
The bear does not eat the tiger.
False
2
inv-proof
[(((triple1) -> rule5) OR ((triple15) -> rule6) OR ((triple9) -> rule6))]
("bear" "eats" "tiger" "-")
((triple1) -> (rule5 % int1))
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int1
((triple15) -> (rule6 % int1))
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int1
((triple9) -> (rule6 % int1))
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int1
The bear does not visit the bear.
True
4
proof
[(((((triple1) -> rule5) triple3) -> rule1) OR ((((triple15) -> rule6) triple3) -> rule1) OR ((((triple9) -> rule6) triple3) -> rule1))]
("bear" "visits" "bear" "-")
((((triple1) -> (rule5 % int2)) triple3) -> (rule1 % int1))
The bear does not visit the bear.
("bear" "visits" "bear" "-")
int1
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int2
((((triple15) -> (rule6 % int2)) triple3) -> (rule1 % int1))
The bear does not visit the bear.
("bear" "visits" "bear" "-")
int1
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int2
((((triple9) -> (rule6 % int2)) triple3) -> (rule1 % int1))
The bear does not visit the bear.
("bear" "visits" "bear" "-")
int1
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int2
The bear visits the bear.
False
4
inv-proof
[(((((triple1) -> rule5) triple3) -> rule1) OR ((((triple15) -> rule6) triple3) -> rule1) OR ((((triple9) -> rule6) triple3) -> rule1))]
("bear" "visits" "bear" "+")
((((triple1) -> (rule5 % int2)) triple3) -> (rule1 % int1))
The bear does not visit the bear.
("bear" "visits" "bear" "-")
int1
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int2
((((triple15) -> (rule6 % int2)) triple3) -> (rule1 % int1))
The bear does not visit the bear.
("bear" "visits" "bear" "-")
int1
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int2
((((triple9) -> (rule6 % int2)) triple3) -> (rule1 % int1))
The bear does not visit the bear.
("bear" "visits" "bear" "-")
int1
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int2
The tiger does not eat the tiger.
Unknown
inv-rconc
[@1: The tiger eats the tiger.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "eats" "tiger" "-")
The squirrel eats the tiger.
Unknown
rconc
[@1: The squirrel eats the tiger.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "eats" "tiger" "+")
The tiger does not like the tiger.
Unknown
inv-rconc
[@1: The tiger likes the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "likes" "tiger" "-")
The squirrel is kind.
Unknown
random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "+")
The squirrel is not young.
Unknown
inv-random
[@0: The squirrel is young.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "young" "-")
The bear is green.
Unknown
random
[@0: The bear is green.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "green" "+")
@0: The bear eats the squirrel.[(triple1)] The bear likes the squirrel.[(triple2)] The bear visits the tiger.[(triple3)] The squirrel eats the bear.[(triple4)] The squirrel is green.[(triple5)] The squirrel is nice.[(triple6)] The squirrel likes the bear.[(triple7 OR ((triple8 triple10) -> rule2))] The squirrel likes the tiger.[(triple8)] The squirrel visits the bear.[(triple9)] The tiger does not like the squirrel.[(triple14)] The tiger does not visit the squirrel.[(triple16)] The tiger eats the bear.[(triple10)] The tiger is green.[(triple11)] The tiger is nice.[(triple12)] The tiger likes the bear.[(triple13)] The tiger visits the bear.[(triple15)] @1: The bear eats the tiger.[(((triple1) -> rule5) OR ((triple15) -> rule6) OR ((triple9) -> rule6))] @2: The bear does not visit the bear.[(((((triple1) -> rule5) triple3) -> rule1) OR ((((triple15) -> rule6) triple3) -> rule1) OR ((((triple9) -> rule6) triple3) -> rule1))]
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
triple1
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
triple2
The bear visits the tiger.
("bear" "visits" "tiger" "+")
triple3
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
triple4
The squirrel is green.
("squirrel" "is" "green" "+")
triple5
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple6
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
triple7
((triple8 triple10) -> (rule2 % int1))
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int1
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
triple8
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
triple9
The tiger does not like the squirrel.
("tiger" "likes" "squirrel" "-")
triple14
The tiger does not visit the squirrel.
("tiger" "visits" "squirrel" "-")
triple16
The tiger eats the bear.
("tiger" "eats" "bear" "+")
triple10
The tiger is green.
("tiger" "is" "green" "+")
triple11
The tiger is nice.
("tiger" "is" "nice" "+")
triple12
The tiger likes the bear.
("tiger" "likes" "bear" "+")
triple13
The tiger visits the bear.
("tiger" "visits" "bear" "+")
triple15
The bear eats the tiger.
("bear" "eats" "tiger" "+")
((triple1) -> (rule5 % int1))
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int1
((triple15) -> (rule6 % int1))
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int1
((triple9) -> (rule6 % int1))
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int1
The bear does not visit the bear.
("bear" "visits" "bear" "-")
((((triple1) -> (rule5 % int2)) triple3) -> (rule1 % int1))
The bear does not visit the bear.
("bear" "visits" "bear" "-")
int1
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int2
((((triple15) -> (rule6 % int2)) triple3) -> (rule1 % int1))
The bear does not visit the bear.
("bear" "visits" "bear" "-")
int1
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int2
((((triple9) -> (rule6 % int2)) triple3) -> (rule1 % int1))
The bear does not visit the bear.
("bear" "visits" "bear" "-")
int1
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int2