The bear is rough. The bear needs the tiger. The bear visits the lion. The lion eats the tiger. The lion is cold. The lion is red. The lion is round. The lion needs the squirrel. The lion does not visit the squirrel. The lion does not visit the tiger. The squirrel visits the bear. The squirrel visits the tiger. The tiger is not red. The tiger does not need the bear. The tiger needs the squirrel. If something needs the bear and it needs the squirrel then the squirrel does not need the lion. If something needs the squirrel and the squirrel needs the bear then the bear is cold. If something eats the bear then the bear eats the tiger. All rough things are round. If something needs the bear then the bear does not eat the squirrel. If something needs the squirrel and it does not visit the tiger then it eats the bear.
The bear is rough.
("bear" "is" "rough" "+")
The bear needs the tiger.
("bear" "needs" "tiger" "+")
The bear visits the lion.
("bear" "visits" "lion" "+")
The lion eats the tiger.
("lion" "eats" "tiger" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is round.
("lion" "is" "round" "+")
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
The lion does not visit the squirrel.
("lion" "visits" "squirrel" "-")
The lion does not visit the tiger.
("lion" "visits" "tiger" "-")
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
The tiger is not red.
("tiger" "is" "red" "-")
The tiger does not need the bear.
("tiger" "needs" "bear" "-")
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
If something needs the bear and it needs the squirrel then the squirrel does not need the lion.
((("something" "needs" "bear" "+") ("something" "needs" "squirrel" "+")) -> ("squirrel" "needs" "lion" "-"))
If something needs the squirrel and the squirrel needs the bear then the bear is cold.
((("something" "needs" "squirrel" "+") ("squirrel" "needs" "bear" "+")) -> ("bear" "is" "cold" "+"))
If something eats the bear then the bear eats the tiger.
((("something" "eats" "bear" "+")) -> ("bear" "eats" "tiger" "+"))
All rough things are round.
((("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
If something needs the bear then the bear does not eat the squirrel.
((("something" "needs" "bear" "+")) -> ("bear" "eats" "squirrel" "-"))
If something needs the squirrel and it does not visit the tiger then it eats the bear.
((("something" "needs" "squirrel" "+") ("something" "visits" "tiger" "~")) -> ("something" "eats" "bear" "+"))
The lion does not visit the squirrel.
True
1
proof
[(triple9)]
("lion" "visits" "squirrel" "-")
triple9
The tiger is red.
False
1
inv-proof
[(triple13)]
("tiger" "is" "red" "+")
triple13
The bear is round.
True
2
proof
[(((triple1) -> rule4))]
("bear" "is" "round" "+")
((triple1) -> (rule4 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The lion does not eat the bear.
False
3
inv-proof
[(((triple8 triple10) -> rule6))]
("lion" "eats" "bear" "-")
((triple8 triple10) -> (rule6 % int1))
The lion eats the bear.
("lion" "eats" "bear" "+")
int1
The bear eats the tiger.
True
4
proof
[(((((triple8 triple10) -> rule6)) -> rule3))]
("bear" "eats" "tiger" "+")
((((triple8 triple10) -> (rule6 % int2))) -> (rule3 % int1))
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int1
The lion eats the bear.
("lion" "eats" "bear" "+")
int2
The bear does not eat the tiger.
False
4
inv-proof
[(((((triple8 triple10) -> rule6)) -> rule3))]
("bear" "eats" "tiger" "-")
((((triple8 triple10) -> (rule6 % int2))) -> (rule3 % int1))
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int1
The lion eats the bear.
("lion" "eats" "bear" "+")
int2
The tiger does not eat the bear.
Unknown
inv-rconc
[@1: The tiger eats the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "eats" "bear" "-")
The squirrel eats the bear.
Unknown
rconc
[@1: The squirrel eats the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "eats" "bear" "+")
The bear is not cold.
Unknown
inv-rconc
[@1: The bear is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "is" "cold" "-")
The lion needs the bear.
Unknown
random
[@0: The lion needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "bear" "+")
The tiger does not visit the squirrel.
Unknown
inv-random
[@0: The tiger visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "squirrel" "-")
The lion needs the lion.
Unknown
random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "+")
@0: The bear is rough.[(triple1)] The bear needs the tiger.[(triple2)] The bear visits the lion.[(triple3)] The lion does not visit the squirrel.[(triple9)] The lion does not visit the tiger.[(triple10)] The lion eats the tiger.[(triple4)] The lion is cold.[(triple5)] The lion is red.[(triple6)] The lion is round.[(triple7)] The lion needs the squirrel.[(triple8)] The squirrel visits the bear.[(triple11)] The squirrel visits the tiger.[(triple12)] The tiger does not need the bear.[(triple14)] The tiger is not red.[(triple13)] The tiger needs the squirrel.[(triple15)] @1: The bear is round.[(((triple1) -> rule4))] The lion eats the bear.[(((triple8 triple10) -> rule6))] @2: The bear eats the tiger.[(((((triple8 triple10) -> rule6)) -> rule3))]
The bear is rough.
("bear" "is" "rough" "+")
triple1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
triple2
The bear visits the lion.
("bear" "visits" "lion" "+")
triple3
The lion does not visit the squirrel.
("lion" "visits" "squirrel" "-")
triple9
The lion does not visit the tiger.
("lion" "visits" "tiger" "-")
triple10
The lion eats the tiger.
("lion" "eats" "tiger" "+")
triple4
The lion is cold.
("lion" "is" "cold" "+")
triple5
The lion is red.
("lion" "is" "red" "+")
triple6
The lion is round.
("lion" "is" "round" "+")
triple7
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
triple8
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
triple11
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
triple12
The tiger does not need the bear.
("tiger" "needs" "bear" "-")
triple14
The tiger is not red.
("tiger" "is" "red" "-")
triple13
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
triple15
The bear is round.
("bear" "is" "round" "+")
((triple1) -> (rule4 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The lion eats the bear.
("lion" "eats" "bear" "+")
((triple8 triple10) -> (rule6 % int1))
The lion eats the bear.
("lion" "eats" "bear" "+")
int1
The bear eats the tiger.
("bear" "eats" "tiger" "+")
((((triple8 triple10) -> (rule6 % int2))) -> (rule3 % int1))
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int1
The lion eats the bear.
("lion" "eats" "bear" "+")
int2