The dog chases the tiger. The tiger is red. If someone is cold then they eat the tiger. If someone eats the tiger then the tiger chases the dog. If someone chases the tiger and the tiger chases the dog then they see the tiger. If the tiger sees the dog then the tiger chases the dog. If someone eats the dog and they are red then the dog sees the tiger. If the dog is round then the dog is young. If someone eats the tiger and they are young then the tiger sees the dog. If someone chases the tiger then the tiger sees the dog.
The dog chases the tiger.
("dog" "chases" "tiger" "+")
The tiger is red.
("tiger" "is" "red" "+")
If someone is cold then they eat the tiger.
((("someone" "is" "cold" "+")) -> ("someone" "eats" "tiger" "+"))
If someone eats the tiger then the tiger chases the dog.
((("someone" "eats" "tiger" "+")) -> ("tiger" "chases" "dog" "+"))
If someone chases the tiger and the tiger chases the dog then they see the tiger.
((("someone" "chases" "tiger" "+") ("tiger" "chases" "dog" "+")) -> ("someone" "sees" "tiger" "+"))
If the tiger sees the dog then the tiger chases the dog.
((("tiger" "sees" "dog" "+")) -> ("tiger" "chases" "dog" "+"))
If someone eats the dog and they are red then the dog sees the tiger.
((("someone" "eats" "dog" "+") ("someone" "is" "red" "+")) -> ("dog" "sees" "tiger" "+"))
If the dog is round then the dog is young.
((("dog" "is" "round" "+")) -> ("dog" "is" "young" "+"))
If someone eats the tiger and they are young then the tiger sees the dog.
((("someone" "eats" "tiger" "+") ("someone" "is" "young" "+")) -> ("tiger" "sees" "dog" "+"))
If someone chases the tiger then the tiger sees the dog.
((("someone" "chases" "tiger" "+")) -> ("tiger" "sees" "dog" "+"))
The tiger is red.
True
1
proof
[(triple2)]
("tiger" "is" "red" "+")
triple2
The dog does not chase the tiger.
False
1
inv-proof
[(triple1)]
("dog" "chases" "tiger" "-")
triple1
The tiger sees the dog.
True
2
proof
[(((triple1) -> rule8))]
("tiger" "sees" "dog" "+")
((triple1) -> (rule8 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
The tiger does not see the dog.
False
2
inv-proof
[(((triple1) -> rule8))]
("tiger" "sees" "dog" "-")
((triple1) -> (rule8 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
The tiger chases the dog.
True
3
proof
[(((((triple1) -> rule8)) -> rule4))]
("tiger" "chases" "dog" "+")
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int1
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int2
The tiger does not chase the dog.
False
3
inv-proof
[(((((triple1) -> rule8)) -> rule4))]
("tiger" "chases" "dog" "-")
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int1
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int2
The dog is not young.
Unknown
inv-rconc
[@1: The dog is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "is" "young" "-")
The dog eats the tiger.
Unknown
rconc
[@1: The dog eats the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "eats" "tiger" "+")
The tiger does not eat the tiger.
Unknown
inv-rconc
[@1: The tiger eats the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "eats" "tiger" "-")
The dog is round.
Unknown
random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "+")
The tiger is not round.
Unknown
inv-random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "-")
The tiger chases the tiger.
Unknown
random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "+")
@0: The dog chases the tiger.[(triple1)] The tiger is red.[(triple2)] @1: The tiger sees the dog.[(((triple1) -> rule8))] @2: The tiger chases the dog.[(((((triple1) -> rule8)) -> rule4))] @3: The dog sees the tiger.[(((triple1 ((((triple1) -> rule8)) -> rule4)) -> rule3))]
The dog chases the tiger.
("dog" "chases" "tiger" "+")
triple1
The tiger is red.
("tiger" "is" "red" "+")
triple2
The tiger sees the dog.
("tiger" "sees" "dog" "+")
((triple1) -> (rule8 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
The tiger chases the dog.
("tiger" "chases" "dog" "+")
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int1
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int2
The dog sees the tiger.
("dog" "sees" "tiger" "+")
((triple1 ((((triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The dog sees the tiger.
("dog" "sees" "tiger" "+")
int1
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int2
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int3