The bear is cold. The cow is not young. The cow does not need the tiger. The cow sees the bear. The dog is round. The dog sees the bear. The tiger needs the bear. The tiger needs the cow. The tiger needs the dog. The tiger sees the cow. If something sees the cow and it does not need the cow then it is big. If something sees the dog and it eats the cow then it is big. If something is cold then it needs the tiger. If something is big and it sees the tiger then it needs the tiger. If something sees the dog then the dog is not cold. If the dog needs the cow then the dog eats the tiger. If something sees the tiger then the tiger is round. If something needs the bear and the bear needs the tiger then the bear sees the tiger.
The bear is cold.
("bear" "is" "cold" "+")
The cow is not young.
("cow" "is" "young" "-")
The cow does not need the tiger.
("cow" "needs" "tiger" "-")
The cow sees the bear.
("cow" "sees" "bear" "+")
The dog is round.
("dog" "is" "round" "+")
The dog sees the bear.
("dog" "sees" "bear" "+")
The tiger needs the bear.
("tiger" "needs" "bear" "+")
The tiger needs the cow.
("tiger" "needs" "cow" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
The tiger sees the cow.
("tiger" "sees" "cow" "+")
If something sees the cow and it does not need the cow then it is big.
((("something" "sees" "cow" "+") ("something" "needs" "cow" "~")) -> ("something" "is" "big" "+"))
If something sees the dog and it eats the cow then it is big.
((("something" "sees" "dog" "+") ("something" "eats" "cow" "+")) -> ("something" "is" "big" "+"))
If something is cold then it needs the tiger.
((("something" "is" "cold" "+")) -> ("something" "needs" "tiger" "+"))
If something is big and it sees the tiger then it needs the tiger.
((("something" "is" "big" "+") ("something" "sees" "tiger" "+")) -> ("something" "needs" "tiger" "+"))
If something sees the dog then the dog is not cold.
((("something" "sees" "dog" "+")) -> ("dog" "is" "cold" "-"))
If the dog needs the cow then the dog eats the tiger.
((("dog" "needs" "cow" "+")) -> ("dog" "eats" "tiger" "+"))
If something sees the tiger then the tiger is round.
((("something" "sees" "tiger" "+")) -> ("tiger" "is" "round" "+"))
If something needs the bear and the bear needs the tiger then the bear sees the tiger.
((("something" "needs" "bear" "+") ("bear" "needs" "tiger" "+")) -> ("bear" "sees" "tiger" "+"))
The dog is round.
True
1
proof
[(triple5)]
("dog" "is" "round" "+")
triple5
The cow is young.
False
1
inv-proof
[(triple2)]
("cow" "is" "young" "+")
triple2
The bear needs the tiger.
True
2
proof
[(((triple1) -> rule3))]
("bear" "needs" "tiger" "+")
((triple1) -> (rule3 % int1))
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int1
The bear does not need the tiger.
False
2
inv-proof
[(((triple1) -> rule3))]
("bear" "needs" "tiger" "-")
((triple1) -> (rule3 % int1))
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int1
The bear sees the tiger.
True
4
proof
[(((triple7 ((triple1) -> rule3)) -> rule8))]
("bear" "sees" "tiger" "+")
((triple7 ((triple1) -> (rule3 % int2))) -> (rule8 % int1))
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int2
The bear does not see the tiger.
False
4
inv-proof
[(((triple7 ((triple1) -> rule3)) -> rule8))]
("bear" "sees" "tiger" "-")
((triple7 ((triple1) -> (rule3 % int2))) -> (rule8 % int1))
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int2
The tiger is round.
True
5
proof
[(((((triple7 ((triple1) -> rule3)) -> rule8)) -> rule7))]
("tiger" "is" "round" "+")
((((triple7 ((triple1) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int2
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int3
The tiger is not round.
False
5
inv-proof
[(((((triple7 ((triple1) -> rule3)) -> rule8)) -> rule7))]
("tiger" "is" "round" "-")
((((triple7 ((triple1) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int2
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int3
The dog does not need the tiger.
Unknown
inv-rconc
[@1: The dog needs the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "needs" "tiger" "-")
The dog is big.
Unknown
rconc
[@1: The dog is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "is" "big" "+")
The bear is not big.
Unknown
inv-rconc
[@1: The bear is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "is" "big" "-")
The tiger needs the tiger.
Unknown
rconc
[@1: The tiger needs the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "needs" "tiger" "+")
The tiger is not cold.
Unknown
inv-random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "-")
The cow is green.
Unknown
random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "+")
The bear does not eat the cow.
Unknown
inv-random
[@0: The bear eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "cow" "-")
The bear eats the bear.
Unknown
random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "+")
@0: The bear is cold.[(triple1)] The cow does not need the tiger.[(triple3)] The cow is not young.[(triple2)] The cow sees the bear.[(triple4)] The dog is round.[(triple5)] The dog sees the bear.[(triple6)] The tiger needs the bear.[(triple7)] The tiger needs the cow.[(triple8)] The tiger needs the dog.[(triple9)] The tiger sees the cow.[(triple10)] @1: The bear needs the tiger.[(((triple1) -> rule3))] @2: The bear sees the tiger.[(((triple7 ((triple1) -> rule3)) -> rule8))] @3: The tiger is round.[(((((triple7 ((triple1) -> rule3)) -> rule8)) -> rule7))]
The bear is cold.
("bear" "is" "cold" "+")
triple1
The cow does not need the tiger.
("cow" "needs" "tiger" "-")
triple3
The cow is not young.
("cow" "is" "young" "-")
triple2
The cow sees the bear.
("cow" "sees" "bear" "+")
triple4
The dog is round.
("dog" "is" "round" "+")
triple5
The dog sees the bear.
("dog" "sees" "bear" "+")
triple6
The tiger needs the bear.
("tiger" "needs" "bear" "+")
triple7
The tiger needs the cow.
("tiger" "needs" "cow" "+")
triple8
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple9
The tiger sees the cow.
("tiger" "sees" "cow" "+")
triple10
The bear needs the tiger.
("bear" "needs" "tiger" "+")
((triple1) -> (rule3 % int1))
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int1
The bear sees the tiger.
("bear" "sees" "tiger" "+")
((triple7 ((triple1) -> (rule3 % int2))) -> (rule8 % int1))
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
((((triple7 ((triple1) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int2
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int3