The bear is not cold. The bear is not rough. The bear needs the dog. The bear does not see the dog. The bear visits the cow. The cow is not cold. The cow needs the tiger. The cow sees the tiger. The dog is nice. The dog does not visit the tiger. The tiger is rough. The tiger visits the dog. If something sees the bear and the bear does not need the cow then the bear visits the cow. All rough things are round. If something sees the bear and the bear sees the cow then the cow visits the tiger. If something needs the cow then it does not visit the cow. If something sees the tiger and the tiger sees the dog then the tiger is cold. If something sees the tiger then the tiger visits the bear. If the dog does not need the tiger then the tiger visits the bear. If something visits the bear then it sees the dog.
The bear is not cold.
("bear" "is" "cold" "-")
The bear is not rough.
("bear" "is" "rough" "-")
The bear needs the dog.
("bear" "needs" "dog" "+")
The bear does not see the dog.
("bear" "sees" "dog" "-")
The bear visits the cow.
("bear" "visits" "cow" "+")
The cow is not cold.
("cow" "is" "cold" "-")
The cow needs the tiger.
("cow" "needs" "tiger" "+")
The cow sees the tiger.
("cow" "sees" "tiger" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog does not visit the tiger.
("dog" "visits" "tiger" "-")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger visits the dog.
("tiger" "visits" "dog" "+")
If something sees the bear and the bear does not need the cow then the bear visits the cow.
((("something" "sees" "bear" "+") ("bear" "needs" "cow" "~")) -> ("bear" "visits" "cow" "+"))
All rough things are round.
((("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
If something sees the bear and the bear sees the cow then the cow visits the tiger.
((("something" "sees" "bear" "+") ("bear" "sees" "cow" "+")) -> ("cow" "visits" "tiger" "+"))
If something needs the cow then it does not visit the cow.
((("something" "needs" "cow" "+")) -> ("something" "visits" "cow" "-"))
If something sees the tiger and the tiger sees the dog then the tiger is cold.
((("something" "sees" "tiger" "+") ("tiger" "sees" "dog" "+")) -> ("tiger" "is" "cold" "+"))
If something sees the tiger then the tiger visits the bear.
((("something" "sees" "tiger" "+")) -> ("tiger" "visits" "bear" "+"))
If the dog does not need the tiger then the tiger visits the bear.
((("dog" "needs" "tiger" "~")) -> ("tiger" "visits" "bear" "+"))
If something visits the bear then it sees the dog.
((("something" "visits" "bear" "+")) -> ("something" "sees" "dog" "+"))
The dog is nice.
True
1
proof
[(triple9)]
("dog" "is" "nice" "+")
triple9
The bear does not need the dog.
False
1
inv-proof
[(triple3)]
("bear" "needs" "dog" "-")
triple3
The tiger visits the bear.
True
2
proof
[(((triple8) -> rule6))]
("tiger" "visits" "bear" "+")
((triple8) -> (rule6 % int1))
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int1
The tiger is not round.
False
2
inv-proof
[(((triple11) -> rule2))]
("tiger" "is" "round" "-")
((triple11) -> (rule2 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger sees the dog.
True
3
proof
[(((((triple8) -> rule6)) -> rule8))]
("tiger" "sees" "dog" "+")
((((triple8) -> (rule6 % int2))) -> (rule8 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int2
The tiger does not see the dog.
False
3
inv-proof
[(((((triple8) -> rule6)) -> rule8))]
("tiger" "sees" "dog" "-")
((((triple8) -> (rule6 % int2))) -> (rule8 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int2
The tiger is cold.
True
5
proof
[(((triple8 ((((triple8) -> rule6)) -> rule8)) -> rule5))]
("tiger" "is" "cold" "+")
((triple8 ((((triple8) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int2
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int3
The tiger is not cold.
False
5
inv-proof
[(((triple8 ((((triple8) -> rule6)) -> rule8)) -> rule5))]
("tiger" "is" "cold" "-")
((triple8 ((((triple8) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int2
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int3
The dog does not see the dog.
Unknown
inv-rconc
[@1: The dog sees the dog.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("dog" "sees" "dog" "-")
The cow sees the dog.
Unknown
rconc
[@1: The cow sees the dog.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cow" "sees" "dog" "+")
The bear is not round.
Unknown
inv-rconc
[@1: The bear is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "is" "round" "-")
The dog is round.
Unknown
rconc
[@1: The dog is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "is" "round" "+")
The cow does not need the dog.
Unknown
inv-random
[@0: The cow needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "dog" "-")
The dog needs the dog.
Unknown
random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "+")
The bear does not need the bear.
Unknown
inv-random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "-")
The dog sees the bear.
Unknown
random
[@0: The dog sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "bear" "+")
@0: The bear does not see the dog.[(triple4)] The bear is not cold.[(triple1)] The bear is not rough.[(triple2)] The bear needs the dog.[(triple3)] The bear visits the cow.[(triple5)] The cow is not cold.[(triple6)] The cow needs the tiger.[(triple7)] The cow sees the tiger.[(triple8)] The dog does not visit the tiger.[(triple10)] The dog is nice.[(triple9)] The tiger is rough.[(triple11)] The tiger visits the dog.[(triple12)] @1: The tiger is round.[(((triple11) -> rule2))] The tiger visits the bear.[(((triple8) -> rule6))] @2: The tiger sees the dog.[(((((triple8) -> rule6)) -> rule8))] @3: The tiger is cold.[(((triple8 ((((triple8) -> rule6)) -> rule8)) -> rule5))]
The bear does not see the dog.
("bear" "sees" "dog" "-")
triple4
The bear is not cold.
("bear" "is" "cold" "-")
triple1
The bear is not rough.
("bear" "is" "rough" "-")
triple2
The bear needs the dog.
("bear" "needs" "dog" "+")
triple3
The bear visits the cow.
("bear" "visits" "cow" "+")
triple5
The cow is not cold.
("cow" "is" "cold" "-")
triple6
The cow needs the tiger.
("cow" "needs" "tiger" "+")
triple7
The cow sees the tiger.
("cow" "sees" "tiger" "+")
triple8
The dog does not visit the tiger.
("dog" "visits" "tiger" "-")
triple10
The dog is nice.
("dog" "is" "nice" "+")
triple9
The tiger is rough.
("tiger" "is" "rough" "+")
triple11
The tiger visits the dog.
("tiger" "visits" "dog" "+")
triple12
The tiger is round.
("tiger" "is" "round" "+")
((triple11) -> (rule2 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger visits the bear.
("tiger" "visits" "bear" "+")
((triple8) -> (rule6 % int1))
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int1
The tiger sees the dog.
("tiger" "sees" "dog" "+")
((((triple8) -> (rule6 % int2))) -> (rule8 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
((triple8 ((((triple8) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int2
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int3