The bear eats the tiger. The bear likes the tiger. The bear visits the dog. The bear visits the tiger. The dog is round. The dog is young. The dog likes the tiger. The dog visits the tiger. The tiger eats the bear. The tiger is blue. If something likes the bear then the bear visits the dog. If something eats the dog and it likes the bear then the dog eats the bear. If something eats the tiger and it is blue then the tiger visits the bear. All young things are big. If something eats the bear then the bear is young. If something eats the tiger then it visits the tiger. All blue things are round. If something visits the bear then the bear likes the tiger.
The bear eats the tiger.
("bear" "eats" "tiger" "+")
The bear likes the tiger.
("bear" "likes" "tiger" "+")
The bear visits the dog.
("bear" "visits" "dog" "+")
The bear visits the tiger.
("bear" "visits" "tiger" "+")
The dog is round.
("dog" "is" "round" "+")
The dog is young.
("dog" "is" "young" "+")
The dog likes the tiger.
("dog" "likes" "tiger" "+")
The dog visits the tiger.
("dog" "visits" "tiger" "+")
The tiger eats the bear.
("tiger" "eats" "bear" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
If something likes the bear then the bear visits the dog.
((("something" "likes" "bear" "+")) -> ("bear" "visits" "dog" "+"))
If something eats the dog and it likes the bear then the dog eats the bear.
((("something" "eats" "dog" "+") ("something" "likes" "bear" "+")) -> ("dog" "eats" "bear" "+"))
If something eats the tiger and it is blue then the tiger visits the bear.
((("something" "eats" "tiger" "+") ("something" "is" "blue" "+")) -> ("tiger" "visits" "bear" "+"))
All young things are big.
((("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
If something eats the bear then the bear is young.
((("something" "eats" "bear" "+")) -> ("bear" "is" "young" "+"))
If something eats the tiger then it visits the tiger.
((("something" "eats" "tiger" "+")) -> ("something" "visits" "tiger" "+"))
All blue things are round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
If something visits the bear then the bear likes the tiger.
((("something" "visits" "bear" "+")) -> ("bear" "likes" "tiger" "+"))
The dog visits the tiger.
True
1
proof
[(triple8)]
("dog" "visits" "tiger" "+")
triple8
The bear does not visit the dog.
False
1
inv-proof
[(triple3)]
("bear" "visits" "dog" "-")
triple3
The dog is big.
True
2
proof
[(((triple6) -> rule4))]
("dog" "is" "big" "+")
((triple6) -> (rule4 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The bear is not young.
False
2
inv-proof
[(((triple9) -> rule5))]
("bear" "is" "young" "-")
((triple9) -> (rule5 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear is big.
True
3
proof
[(((((triple9) -> rule5)) -> rule4))]
("bear" "is" "big" "+")
((((triple9) -> (rule5 % int2))) -> (rule4 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
The bear is not big.
False
3
inv-proof
[(((((triple9) -> rule5)) -> rule4))]
("bear" "is" "big" "-")
((((triple9) -> (rule5 % int2))) -> (rule4 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
The tiger does not visit the bear.
Unknown
inv-rconc
[@1: The tiger visits the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "visits" "bear" "-")
The dog eats the bear.
Unknown
rconc
[@1: The dog eats the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "eats" "bear" "+")
The bear is not round.
Unknown
inv-rconc
[@1: The bear is round.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bear" "is" "round" "-")
The bear visits the bear.
Unknown
random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "+")
The tiger is not young.
Unknown
inv-random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "-")
The dog visits the dog.
Unknown
random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "+")
@0: The bear eats the tiger.[(triple1)] The bear likes the tiger.[(triple2)] The bear visits the dog.[(triple3)] The bear visits the tiger.[(triple4 OR ((triple1) -> rule6))] The dog is round.[(triple5)] The dog is young.[(triple6)] The dog likes the tiger.[(triple7)] The dog visits the tiger.[(triple8)] The tiger eats the bear.[(triple9)] The tiger is blue.[(triple10)] @1: The bear is young.[(((triple9) -> rule5))] The dog is big.[(((triple6) -> rule4))] The tiger is round.[(((triple10) -> rule7))] @2: The bear is big.[(((((triple9) -> rule5)) -> rule4))]
The bear eats the tiger.
("bear" "eats" "tiger" "+")
triple1
The bear likes the tiger.
("bear" "likes" "tiger" "+")
triple2
The bear visits the dog.
("bear" "visits" "dog" "+")
triple3
The bear visits the tiger.
("bear" "visits" "tiger" "+")
triple4
((triple1) -> (rule6 % int1))
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int1
The dog is round.
("dog" "is" "round" "+")
triple5
The dog is young.
("dog" "is" "young" "+")
triple6
The dog likes the tiger.
("dog" "likes" "tiger" "+")
triple7
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple8
The tiger eats the bear.
("tiger" "eats" "bear" "+")
triple9
The tiger is blue.
("tiger" "is" "blue" "+")
triple10
The bear is young.
("bear" "is" "young" "+")
((triple9) -> (rule5 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The dog is big.
("dog" "is" "big" "+")
((triple6) -> (rule4 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
((triple10) -> (rule7 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The bear is big.
("bear" "is" "big" "+")
((((triple9) -> (rule5 % int2))) -> (rule4 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2