The bear is round. The cow eats the bear. The dog chases the cow. The tiger eats the cow. If someone eats the tiger then the tiger is blue. If someone likes the bear and the bear is not blue then the bear is not kind. If someone likes the bear then the bear chases the cow. If the tiger chases the cow then the cow does not like the dog. If someone chases the cow then the cow does not chase the bear. If someone eats the cow then the cow eats the tiger.
The bear is round.
("bear" "is" "round" "+")
The cow eats the bear.
("cow" "eats" "bear" "+")
The dog chases the cow.
("dog" "chases" "cow" "+")
The tiger eats the cow.
("tiger" "eats" "cow" "+")
If someone eats the tiger then the tiger is blue.
((("someone" "eats" "tiger" "+")) -> ("tiger" "is" "blue" "+"))
If someone likes the bear and the bear is not blue then the bear is not kind.
((("someone" "likes" "bear" "+") ("bear" "is" "blue" "~")) -> ("bear" "is" "kind" "-"))
If someone likes the bear then the bear chases the cow.
((("someone" "likes" "bear" "+")) -> ("bear" "chases" "cow" "+"))
If the tiger chases the cow then the cow does not like the dog.
((("tiger" "chases" "cow" "+")) -> ("cow" "likes" "dog" "-"))
If someone chases the cow then the cow does not chase the bear.
((("someone" "chases" "cow" "+")) -> ("cow" "chases" "bear" "-"))
If someone eats the cow then the cow eats the tiger.
((("someone" "eats" "cow" "+")) -> ("cow" "eats" "tiger" "+"))
The tiger eats the cow.
True
1
proof
[(triple4)]
("tiger" "eats" "cow" "+")
triple4
The dog does not chase the cow.
False
1
inv-proof
[(triple3)]
("dog" "chases" "cow" "-")
triple3
The cow does not chase the bear.
True
2
proof
[(((triple3) -> rule5))]
("cow" "chases" "bear" "-")
((triple3) -> (rule5 % int1))
The cow does not chase the bear.
("cow" "chases" "bear" "-")
int1
The cow does not eat the tiger.
False
2
inv-proof
[(((triple4) -> rule6))]
("cow" "eats" "tiger" "-")
((triple4) -> (rule6 % int1))
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int1
The tiger is blue.
True
3
proof
[(((((triple4) -> rule6)) -> rule1))]
("tiger" "is" "blue" "+")
((((triple4) -> (rule6 % int2))) -> (rule1 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int2
The tiger is not blue.
False
3
inv-proof
[(((((triple4) -> rule6)) -> rule1))]
("tiger" "is" "blue" "-")
((((triple4) -> (rule6 % int2))) -> (rule1 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int2
The bear does not chase the cow.
Unknown
inv-rconc
[@1: The bear chases the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "chases" "cow" "-")
The tiger likes the cow.
Unknown
random
[@0: The tiger likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "cow" "+")
The bear does not eat the tiger.
Unknown
inv-random
[@0: The bear eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "tiger" "-")
The cow likes the bear.
Unknown
random
[@0: The cow likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "bear" "+")
The tiger is not kind.
Unknown
inv-random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "-")
The dog is rough.
Unknown
random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "+")
@0: The bear is round.[(triple1)] The cow eats the bear.[(triple2)] The dog chases the cow.[(triple3)] The tiger eats the cow.[(triple4)] @1: The cow does not chase the bear.[(((triple3) -> rule5))] The cow eats the tiger.[(((triple4) -> rule6))] @2: The tiger is blue.[(((((triple4) -> rule6)) -> rule1))]
The bear is round.
("bear" "is" "round" "+")
triple1
The cow eats the bear.
("cow" "eats" "bear" "+")
triple2
The dog chases the cow.
("dog" "chases" "cow" "+")
triple3
The tiger eats the cow.
("tiger" "eats" "cow" "+")
triple4
The cow does not chase the bear.
("cow" "chases" "bear" "-")
((triple3) -> (rule5 % int1))
The cow does not chase the bear.
("cow" "chases" "bear" "-")
int1
The cow eats the tiger.
("cow" "eats" "tiger" "+")
((triple4) -> (rule6 % int1))
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
((((triple4) -> (rule6 % int2))) -> (rule1 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int2