The bear sees the lion. The bear does not see the tiger. The bear visits the tiger. The cow sees the tiger. The cow visits the bear. The cow visits the tiger. The lion is blue. The lion is young. The lion sees the cow. The lion does not see the tiger. The lion does not visit the cow. The tiger is green. The tiger is young. The tiger does not like the lion. The tiger sees the cow. The tiger visits the bear. If the bear is green and the bear sees the lion then the lion sees the bear. If someone likes the cow then they are young. If someone sees the lion then they are green.
The bear sees the lion.
("bear" "sees" "lion" "+")
The bear does not see the tiger.
("bear" "sees" "tiger" "-")
The bear visits the tiger.
("bear" "visits" "tiger" "+")
The cow sees the tiger.
("cow" "sees" "tiger" "+")
The cow visits the bear.
("cow" "visits" "bear" "+")
The cow visits the tiger.
("cow" "visits" "tiger" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is young.
("lion" "is" "young" "+")
The lion sees the cow.
("lion" "sees" "cow" "+")
The lion does not see the tiger.
("lion" "sees" "tiger" "-")
The lion does not visit the cow.
("lion" "visits" "cow" "-")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger does not like the lion.
("tiger" "likes" "lion" "-")
The tiger sees the cow.
("tiger" "sees" "cow" "+")
The tiger visits the bear.
("tiger" "visits" "bear" "+")
If the bear is green and the bear sees the lion then the lion sees the bear.
((("bear" "is" "green" "+") ("bear" "sees" "lion" "+")) -> ("lion" "sees" "bear" "+"))
If someone likes the cow then they are young.
((("someone" "likes" "cow" "+")) -> ("someone" "is" "young" "+"))
If someone sees the lion then they are green.
((("someone" "sees" "lion" "+")) -> ("someone" "is" "green" "+"))
The tiger is young.
True
1
proof
[(triple13)]
("tiger" "is" "young" "+")
triple13
The tiger does not see the cow.
False
1
inv-proof
[(triple15)]
("tiger" "sees" "cow" "-")
triple15
The cow is not green.
Unknown
inv-rconc
[@1: The cow is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "is" "green" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
@0: The bear does not see the tiger.[(triple2)] The bear sees the lion.[(triple1)] The bear visits the tiger.[(triple3)] The cow sees the tiger.[(triple4)] The cow visits the bear.[(triple5)] The cow visits the tiger.[(triple6)] The lion does not see the tiger.[(triple10)] The lion does not visit the cow.[(triple11)] The lion is blue.[(triple7)] The lion is young.[(triple8)] The lion sees the cow.[(triple9)] The tiger does not like the lion.[(triple14)] The tiger is green.[(triple12)] The tiger is young.[(triple13)] The tiger sees the cow.[(triple15)] The tiger visits the bear.[(triple16)] @1: The bear is green.[(((triple1) -> rule3))] @2: The lion sees the bear.[(((((triple1) -> rule3) triple1) -> rule1))]
The bear does not see the tiger.
("bear" "sees" "tiger" "-")
triple2
The bear sees the lion.
("bear" "sees" "lion" "+")
triple1
The bear visits the tiger.
("bear" "visits" "tiger" "+")
triple3
The cow sees the tiger.
("cow" "sees" "tiger" "+")
triple4
The cow visits the bear.
("cow" "visits" "bear" "+")
triple5
The cow visits the tiger.
("cow" "visits" "tiger" "+")
triple6
The lion does not see the tiger.
("lion" "sees" "tiger" "-")
triple10
The lion does not visit the cow.
("lion" "visits" "cow" "-")
triple11
The lion is blue.
("lion" "is" "blue" "+")
triple7
The lion is young.
("lion" "is" "young" "+")
triple8
The lion sees the cow.
("lion" "sees" "cow" "+")
triple9
The tiger does not like the lion.
("tiger" "likes" "lion" "-")
triple14
The tiger is green.
("tiger" "is" "green" "+")
triple12
The tiger is young.
("tiger" "is" "young" "+")
triple13
The tiger sees the cow.
("tiger" "sees" "cow" "+")
triple15
The tiger visits the bear.
("tiger" "visits" "bear" "+")
triple16
The bear is green.
("bear" "is" "green" "+")
((triple1) -> (rule3 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The lion sees the bear.
("lion" "sees" "bear" "+")
((((triple1) -> (rule3 % int2)) triple1) -> (rule1 % int1))
The lion sees the bear.
("lion" "sees" "bear" "+")
int1
The bear is green.
("bear" "is" "green" "+")
int2