The cat is green. The tiger is green. If someone visits the cat then the cat visits the tiger. If someone is green then they visit the cat. If someone is kind and they need the cat then they visit the tiger. If someone is round and they need the tiger then the tiger is round. If someone visits the cat then they need the tiger. If the cat chases the tiger then the tiger needs the cat. If someone is round and they visit the tiger then the tiger visits the cat. If someone is nice then they need the tiger.
The cat is green.
("cat" "is" "green" "+")
The tiger is green.
("tiger" "is" "green" "+")
If someone visits the cat then the cat visits the tiger.
((("someone" "visits" "cat" "+")) -> ("cat" "visits" "tiger" "+"))
If someone is green then they visit the cat.
((("someone" "is" "green" "+")) -> ("someone" "visits" "cat" "+"))
If someone is kind and they need the cat then they visit the tiger.
((("someone" "is" "kind" "+") ("someone" "needs" "cat" "+")) -> ("someone" "visits" "tiger" "+"))
If someone is round and they need the tiger then the tiger is round.
((("someone" "is" "round" "+") ("someone" "needs" "tiger" "+")) -> ("tiger" "is" "round" "+"))
If someone visits the cat then they need the tiger.
((("someone" "visits" "cat" "+")) -> ("someone" "needs" "tiger" "+"))
If the cat chases the tiger then the tiger needs the cat.
((("cat" "chases" "tiger" "+")) -> ("tiger" "needs" "cat" "+"))
If someone is round and they visit the tiger then the tiger visits the cat.
((("someone" "is" "round" "+") ("someone" "visits" "tiger" "+")) -> ("tiger" "visits" "cat" "+"))
If someone is nice then they need the tiger.
((("someone" "is" "nice" "+")) -> ("someone" "needs" "tiger" "+"))
The cat is green.
True
1
proof
[(triple1)]
("cat" "is" "green" "+")
triple1
The tiger is not green.
False
1
inv-proof
[(triple2)]
("tiger" "is" "green" "-")
triple2
The cat visits the cat.
True
2
proof
[(((triple1) -> rule2))]
("cat" "visits" "cat" "+")
((triple1) -> (rule2 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat does not visit the cat.
False
2
inv-proof
[(((triple1) -> rule2))]
("cat" "visits" "cat" "-")
((triple1) -> (rule2 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat visits the tiger.
True
3
proof
[(((((triple1) -> rule2)) -> rule1) OR ((((triple2) -> rule2)) -> rule1))]
("cat" "visits" "tiger" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int1
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int2
The tiger does not need the tiger.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule5))]
("tiger" "needs" "tiger" "-")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int2
The tiger does not need the cat.
Unknown
inv-rconc
[@1: The tiger needs the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "needs" "cat" "-")
The tiger is round.
Unknown
rconc
[@1: The tiger is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "is" "round" "+")
The tiger does not visit the tiger.
Unknown
inv-rconc
[@1: The tiger visits the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "visits" "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 is not red.
Unknown
inv-random
[@0: The cat is red.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "red" "-")
The tiger is red.
Unknown
random
[@0: The tiger is red.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "red" "+")
@0: The cat is green.[(triple1)] The tiger is green.[(triple2)] @1: The cat visits the cat.[(((triple1) -> rule2))] The tiger visits the cat.[(((triple2) -> rule2))] @2: The cat needs the tiger.[(((((triple1) -> rule2)) -> rule5))] The cat visits the tiger.[(((((triple1) -> rule2)) -> rule1) OR ((((triple2) -> rule2)) -> rule1))] The tiger needs the tiger.[(((((triple2) -> rule2)) -> rule5))]
The cat is green.
("cat" "is" "green" "+")
triple1
The tiger is green.
("tiger" "is" "green" "+")
triple2
The cat visits the cat.
("cat" "visits" "cat" "+")
((triple1) -> (rule2 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The tiger visits the cat.
("tiger" "visits" "cat" "+")
((triple2) -> (rule2 % int1))
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int1
The cat needs the tiger.
("cat" "needs" "tiger" "+")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat visits the tiger.
("cat" "visits" "tiger" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int1
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int2
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int2