The cat chases the tiger. The tiger visits the cat. If someone sees the cat then the cat visits the tiger. If someone sees the cat then the cat is cold. If someone visits the cat then they are young. If someone chases the tiger then they visit the tiger. If someone visits the cat then they chase the tiger. If someone visits the tiger then they are blue.
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
If someone sees the cat then the cat visits the tiger.
((("someone" "sees" "cat" "+")) -> ("cat" "visits" "tiger" "+"))
If someone sees the cat then the cat is cold.
((("someone" "sees" "cat" "+")) -> ("cat" "is" "cold" "+"))
If someone visits the cat then they are young.
((("someone" "visits" "cat" "+")) -> ("someone" "is" "young" "+"))
If someone chases the tiger then they visit the tiger.
((("someone" "chases" "tiger" "+")) -> ("someone" "visits" "tiger" "+"))
If someone visits the cat then they chase the tiger.
((("someone" "visits" "cat" "+")) -> ("someone" "chases" "tiger" "+"))
If someone visits the tiger then they are blue.
((("someone" "visits" "tiger" "+")) -> ("someone" "is" "blue" "+"))
The cat chases the tiger.
True
1
proof
[(triple1)]
("cat" "chases" "tiger" "+")
triple1
The tiger does not visit the cat.
False
1
inv-proof
[(triple2)]
("tiger" "visits" "cat" "-")
triple2
The tiger is young.
True
2
proof
[(((triple2) -> rule3))]
("tiger" "is" "young" "+")
((triple2) -> (rule3 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is not young.
False
2
inv-proof
[(((triple2) -> rule3))]
("tiger" "is" "young" "-")
((triple2) -> (rule3 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The cat is not cold.
Unknown
inv-rconc
[@1: The cat is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "is" "cold" "-")
The cat is young.
Unknown
rconc
[@1: The cat is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "is" "young" "+")
The tiger is not cold.
Unknown
inv-random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "-")
The cat visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
@0: The cat chases the tiger.[(triple1)] The tiger visits the cat.[(triple2)] @1: The cat visits the tiger.[(((triple1) -> rule4))] The tiger chases the tiger.[(((triple2) -> rule5))] The tiger is young.[(((triple2) -> rule3))] @2: The cat is blue.[(((((triple1) -> rule4)) -> rule6))] The tiger visits the tiger.[(((((triple2) -> rule5)) -> rule4))] @3: The tiger is blue.[(((((((triple2) -> rule5)) -> rule4)) -> rule6))]
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple1
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple2
The cat visits the tiger.
("cat" "visits" "tiger" "+")
((triple1) -> (rule4 % int1))
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
((triple2) -> (rule5 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
((triple2) -> (rule3 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int2
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int2
The tiger is blue.
("tiger" "is" "blue" "+")
((((((triple2) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int3