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