The dog sees the tiger. The tiger is big. The tiger sees the dog. If the dog sees the tiger and the dog needs the tiger then the tiger is red. If something sees the tiger then it needs the tiger.
The dog sees the tiger.
("dog" "sees" "tiger" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger sees the dog.
("tiger" "sees" "dog" "+")
If the dog sees the tiger and the dog needs the tiger then the tiger is red.
((("dog" "sees" "tiger" "+") ("dog" "needs" "tiger" "+")) -> ("tiger" "is" "red" "+"))
If something sees the tiger then it needs the tiger.
((("something" "sees" "tiger" "+")) -> ("something" "needs" "tiger" "+"))
The tiger is big.
True
1
proof
[(triple2)]
("tiger" "is" "big" "+")
triple2
The dog does not see the tiger.
False
1
inv-proof
[(triple1)]
("dog" "sees" "tiger" "-")
triple1
The dog needs the tiger.
True
2
proof
[(((triple1) -> rule2))]
("dog" "needs" "tiger" "+")
((triple1) -> (rule2 % int1))
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int1
The dog does not need the tiger.
False
2
inv-proof
[(((triple1) -> rule2))]
("dog" "needs" "tiger" "-")
((triple1) -> (rule2 % int1))
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int1
The tiger is red.
True
4
proof
[(((triple1 ((triple1) -> rule2)) -> rule1))]
("tiger" "is" "red" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int2
The tiger is not red.
False
4
inv-proof
[(((triple1 ((triple1) -> rule2)) -> rule1))]
("tiger" "is" "red" "-")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int2
The tiger does not need the tiger.
Unknown
inv-rconc
[@1: The tiger needs the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "needs" "tiger" "-")
The dog is cold.
Unknown
random
[@0: The dog is cold.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "cold" "+")
The tiger is not round.
Unknown
inv-random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "-")
The tiger is kind.
Unknown
random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "+")
The dog is not big.
Unknown
inv-random
[@0: The dog is big.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "big" "-")
The dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
@0: The dog sees the tiger.[(triple1)] The tiger is big.[(triple2)] The tiger sees the dog.[(triple3)] @1: The dog needs the tiger.[(((triple1) -> rule2))] @2: The tiger is red.[(((triple1 ((triple1) -> rule2)) -> rule1))]
The dog sees the tiger.
("dog" "sees" "tiger" "+")
triple1
The tiger is big.
("tiger" "is" "big" "+")
triple2
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple3
The dog needs the tiger.
("dog" "needs" "tiger" "+")
((triple1) -> (rule2 % int1))
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int2