The cat chases the tiger. The cat is kind. The cat is young. The tiger chases the cat. The tiger eats the cat. The tiger is cold. The tiger is kind. The tiger is not red. The tiger is not young. The tiger sees the cat. If someone sees the tiger then they chase the tiger. If someone eats the cat then the cat does not eat the tiger.
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is young.
("cat" "is" "young" "+")
The tiger chases the cat.
("tiger" "chases" "cat" "+")
The tiger eats the cat.
("tiger" "eats" "cat" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is not red.
("tiger" "is" "red" "-")
The tiger is not young.
("tiger" "is" "young" "-")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
If someone sees the tiger then they chase the tiger.
((("someone" "sees" "tiger" "+")) -> ("someone" "chases" "tiger" "+"))
If someone eats the cat then the cat does not eat the tiger.
((("someone" "eats" "cat" "+")) -> ("cat" "eats" "tiger" "-"))
The cat chases the tiger.
True
1
proof
[(triple1)]
("cat" "chases" "tiger" "+")
triple1
The cat is not young.
False
1
inv-proof
[(triple3)]
("cat" "is" "young" "-")
triple3
The cat does not eat the tiger.
True
2
proof
[(((triple5) -> rule2))]
("cat" "eats" "tiger" "-")
((triple5) -> (rule2 % int1))
The cat does not eat the tiger.
("cat" "eats" "tiger" "-")
int1
The cat eats the tiger.
False
2
inv-proof
[(((triple5) -> rule2))]
("cat" "eats" "tiger" "+")
((triple5) -> (rule2 % int1))
The cat does not eat the tiger.
("cat" "eats" "tiger" "-")
int1
The tiger does not chase the tiger.
Unknown
inv-rconc
[@1: The tiger chases the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "chases" "tiger" "-")
The cat chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
The cat does not eat the cat.
Unknown
inv-random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "-")
The cat is red.
Unknown
random
[@0: The cat is red.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "red" "+")
@0: The cat chases the tiger.[(triple1)] The cat is kind.[(triple2)] The cat is young.[(triple3)] The tiger chases the cat.[(triple4)] The tiger eats the cat.[(triple5)] The tiger is cold.[(triple6)] The tiger is kind.[(triple7)] The tiger is not red.[(triple8)] The tiger is not young.[(triple9)] The tiger sees the cat.[(triple10)] @1: The cat does not eat the tiger.[(((triple5) -> rule2))]
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple1
The cat is kind.
("cat" "is" "kind" "+")
triple2
The cat is young.
("cat" "is" "young" "+")
triple3
The tiger chases the cat.
("tiger" "chases" "cat" "+")
triple4
The tiger eats the cat.
("tiger" "eats" "cat" "+")
triple5
The tiger is cold.
("tiger" "is" "cold" "+")
triple6
The tiger is kind.
("tiger" "is" "kind" "+")
triple7
The tiger is not red.
("tiger" "is" "red" "-")
triple8
The tiger is not young.
("tiger" "is" "young" "-")
triple9
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple10
The cat does not eat the tiger.
("cat" "eats" "tiger" "-")
((triple5) -> (rule2 % int1))
The cat does not eat the tiger.
("cat" "eats" "tiger" "-")
int1