The bear is big. The bear is blue. The bear is round. The bear likes the cow. The bear needs the cow. The bear sees the cat. The bear sees the cow. The cat is blue. The cat needs the cow. The cat sees the bear. The cat sees the cow. The cow is blue. The cow is kind. The cow needs the bear. The cow needs the cat. The cow sees the cat. If something is big and round then it likes the bear. If something is big then it likes the bear. If something is rough then it likes the cow. If the bear is rough and the bear needs the cat then the bear is round. If something sees the bear and it is big then the bear is kind. If the cat needs the bear and the bear likes the cat then the bear is round. If the cow needs the bear then the cow is rough. All rough things are round.
The bear is big.
("bear" "is" "big" "+")
The bear is blue.
("bear" "is" "blue" "+")
The bear is round.
("bear" "is" "round" "+")
The bear likes the cow.
("bear" "likes" "cow" "+")
The bear needs the cow.
("bear" "needs" "cow" "+")
The bear sees the cat.
("bear" "sees" "cat" "+")
The bear sees the cow.
("bear" "sees" "cow" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat needs the cow.
("cat" "needs" "cow" "+")
The cat sees the bear.
("cat" "sees" "bear" "+")
The cat sees the cow.
("cat" "sees" "cow" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow needs the bear.
("cow" "needs" "bear" "+")
The cow needs the cat.
("cow" "needs" "cat" "+")
The cow sees the cat.
("cow" "sees" "cat" "+")
If something is big and round then it likes the bear.
((("something" "is" "big" "+") ("something" "is" "round" "+")) -> ("something" "likes" "bear" "+"))
If something is big then it likes the bear.
((("something" "is" "big" "+")) -> ("something" "likes" "bear" "+"))
If something is rough then it likes the cow.
((("something" "is" "rough" "+")) -> ("something" "likes" "cow" "+"))
If the bear is rough and the bear needs the cat then the bear is round.
((("bear" "is" "rough" "+") ("bear" "needs" "cat" "+")) -> ("bear" "is" "round" "+"))
If something sees the bear and it is big then the bear is kind.
((("something" "sees" "bear" "+") ("something" "is" "big" "+")) -> ("bear" "is" "kind" "+"))
If the cat needs the bear and the bear likes the cat then the bear is round.
((("cat" "needs" "bear" "+") ("bear" "likes" "cat" "+")) -> ("bear" "is" "round" "+"))
If the cow needs the bear then the cow is rough.
((("cow" "needs" "bear" "+")) -> ("cow" "is" "rough" "+"))
All rough things are round.
((("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
The cow is blue.
True
1
proof
[(triple12)]
("cow" "is" "blue" "+")
triple12
The bear does not see the cat.
False
1
inv-proof
[(triple6)]
("bear" "sees" "cat" "-")
triple6
The bear likes the bear.
True
2
proof
[(((triple1) -> rule2) OR ((triple1 triple3) -> rule1))]
("bear" "likes" "bear" "+")
((triple1) -> (rule2 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
((triple1 triple3) -> (rule1 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear does not like the bear.
False
2
inv-proof
[(((triple1) -> rule2) OR ((triple1 triple3) -> rule1))]
("bear" "likes" "bear" "-")
((triple1) -> (rule2 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
((triple1 triple3) -> (rule1 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The cow likes the cow.
True
3
proof
[(((((triple14) -> rule7)) -> rule3))]
("cow" "likes" "cow" "+")
((((triple14) -> (rule7 % int2))) -> (rule3 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow is not round.
False
3
inv-proof
[(((((triple14) -> rule7)) -> rule8))]
("cow" "is" "round" "-")
((((triple14) -> (rule7 % int2))) -> (rule8 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cat does not like the cow.
Unknown
inv-rconc
[@1: The cat likes the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "likes" "cow" "-")
The cow likes the bear.
Unknown
rconc
[@1: The cow likes the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "likes" "bear" "+")
The cat does not like the bear.
Unknown
inv-rconc
[@1: The cat likes the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "likes" "bear" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
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 cat is big.
Unknown
random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "+")
@0: The bear is big.[(triple1)] The bear is blue.[(triple2)] The bear is round.[(triple3)] The bear likes the cow.[(triple4)] The bear needs the cow.[(triple5)] The bear sees the cat.[(triple6)] The bear sees the cow.[(triple7)] The cat is blue.[(triple8)] The cat needs the cow.[(triple9)] The cat sees the bear.[(triple10)] The cat sees the cow.[(triple11)] The cow is blue.[(triple12)] The cow is kind.[(triple13)] The cow needs the bear.[(triple14)] The cow needs the cat.[(triple15)] The cow sees the cat.[(triple16)] @1: The bear likes the bear.[(((triple1) -> rule2) OR ((triple1 triple3) -> rule1))] The cow is rough.[(((triple14) -> rule7))] @2: The cow is round.[(((((triple14) -> rule7)) -> rule8))] The cow likes the cow.[(((((triple14) -> rule7)) -> rule3))]
The bear is big.
("bear" "is" "big" "+")
triple1
The bear is blue.
("bear" "is" "blue" "+")
triple2
The bear is round.
("bear" "is" "round" "+")
triple3
The bear likes the cow.
("bear" "likes" "cow" "+")
triple4
The bear needs the cow.
("bear" "needs" "cow" "+")
triple5
The bear sees the cat.
("bear" "sees" "cat" "+")
triple6
The bear sees the cow.
("bear" "sees" "cow" "+")
triple7
The cat is blue.
("cat" "is" "blue" "+")
triple8
The cat needs the cow.
("cat" "needs" "cow" "+")
triple9
The cat sees the bear.
("cat" "sees" "bear" "+")
triple10
The cat sees the cow.
("cat" "sees" "cow" "+")
triple11
The cow is blue.
("cow" "is" "blue" "+")
triple12
The cow is kind.
("cow" "is" "kind" "+")
triple13
The cow needs the bear.
("cow" "needs" "bear" "+")
triple14
The cow needs the cat.
("cow" "needs" "cat" "+")
triple15
The cow sees the cat.
("cow" "sees" "cat" "+")
triple16
The bear likes the bear.
("bear" "likes" "bear" "+")
((triple1) -> (rule2 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
((triple1 triple3) -> (rule1 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
((triple14) -> (rule7 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is round.
("cow" "is" "round" "+")
((((triple14) -> (rule7 % int2))) -> (rule8 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow likes the cow.
("cow" "likes" "cow" "+")
((((triple14) -> (rule7 % int2))) -> (rule3 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2