The bear is red. The cow eats the tiger. The dog visits the bear. The tiger is nice. If someone visits the dog then the dog sees the bear. If someone visits the dog and they eat the cow then the cow visits the dog. If someone sees the bear and the bear eats the tiger then they visit the dog. If someone visits the tiger then the tiger sees the dog. If someone is nice then they are big. If someone is big then they visit the tiger.
The bear is red.
("bear" "is" "red" "+")
The cow eats the tiger.
("cow" "eats" "tiger" "+")
The dog visits the bear.
("dog" "visits" "bear" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
If someone visits the dog then the dog sees the bear.
((("someone" "visits" "dog" "+")) -> ("dog" "sees" "bear" "+"))
If someone visits the dog and they eat the cow then the cow visits the dog.
((("someone" "visits" "dog" "+") ("someone" "eats" "cow" "+")) -> ("cow" "visits" "dog" "+"))
If someone sees the bear and the bear eats the tiger then they visit the dog.
((("someone" "sees" "bear" "+") ("bear" "eats" "tiger" "+")) -> ("someone" "visits" "dog" "+"))
If someone visits the tiger then the tiger sees the dog.
((("someone" "visits" "tiger" "+")) -> ("tiger" "sees" "dog" "+"))
If someone is nice then they are big.
((("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
If someone is big then they visit the tiger.
((("someone" "is" "big" "+")) -> ("someone" "visits" "tiger" "+"))
The tiger is nice.
True
1
proof
[(triple4)]
("tiger" "is" "nice" "+")
triple4
The dog does not visit the bear.
False
1
inv-proof
[(triple3)]
("dog" "visits" "bear" "-")
triple3
The tiger is big.
True
2
proof
[(((triple4) -> rule5))]
("tiger" "is" "big" "+")
((triple4) -> (rule5 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is not big.
False
2
inv-proof
[(((triple4) -> rule5))]
("tiger" "is" "big" "-")
((triple4) -> (rule5 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger visits the tiger.
True
3
proof
[(((((triple4) -> rule5)) -> rule6))]
("tiger" "visits" "tiger" "+")
((((triple4) -> (rule5 % int2))) -> (rule6 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger does not visit the tiger.
False
3
inv-proof
[(((((triple4) -> rule5)) -> rule6))]
("tiger" "visits" "tiger" "-")
((((triple4) -> (rule5 % int2))) -> (rule6 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger sees the dog.
True
4
proof
[(((((((triple4) -> rule5)) -> rule6)) -> rule4))]
("tiger" "sees" "dog" "+")
((((((triple4) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
The tiger does not see the dog.
False
4
inv-proof
[(((((((triple4) -> rule5)) -> rule6)) -> rule4))]
("tiger" "sees" "dog" "-")
((((((triple4) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
The cow is not big.
Unknown
inv-rconc
[@1: The cow is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "is" "big" "-")
The bear visits the tiger.
Unknown
rconc
[@2: The bear visits the tiger.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("bear" "visits" "tiger" "+")
The dog does not see the bear.
Unknown
inv-rconc
[@2: The dog sees the bear.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("dog" "sees" "bear" "-")
The cow visits the dog.
Unknown
rconc
[@1: The cow visits the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "visits" "dog" "+")
The dog does not eat the cow.
Unknown
inv-random
[@0: The dog eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "cow" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
The tiger does not see the tiger.
Unknown
inv-random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "-")
The dog visits the cow.
Unknown
random
[@0: The dog visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "cow" "+")
@0: The bear is red.[(triple1)] The cow eats the tiger.[(triple2)] The dog visits the bear.[(triple3)] The tiger is nice.[(triple4)] @1: The tiger is big.[(((triple4) -> rule5))] @2: The tiger visits the tiger.[(((((triple4) -> rule5)) -> rule6))] @3: The tiger sees the dog.[(((((((triple4) -> rule5)) -> rule6)) -> rule4))]
The bear is red.
("bear" "is" "red" "+")
triple1
The cow eats the tiger.
("cow" "eats" "tiger" "+")
triple2
The dog visits the bear.
("dog" "visits" "bear" "+")
triple3
The tiger is nice.
("tiger" "is" "nice" "+")
triple4
The tiger is big.
("tiger" "is" "big" "+")
((triple4) -> (rule5 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
((((triple4) -> (rule5 % int2))) -> (rule6 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger sees the dog.
("tiger" "sees" "dog" "+")
((((((triple4) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3