The dog does not visit the tiger. The squirrel is red. The tiger sees the squirrel. If someone visits the tiger then they are cold. If the dog is cold and the dog is round then the dog likes the tiger. If someone sees the squirrel then they visit the tiger.
The dog does not visit the tiger.
("dog" "visits" "tiger" "-")
The squirrel is red.
("squirrel" "is" "red" "+")
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
If someone visits the tiger then they are cold.
((("someone" "visits" "tiger" "+")) -> ("someone" "is" "cold" "+"))
If the dog is cold and the dog is round then the dog likes the tiger.
((("dog" "is" "cold" "+") ("dog" "is" "round" "+")) -> ("dog" "likes" "tiger" "+"))
If someone sees the squirrel then they visit the tiger.
((("someone" "sees" "squirrel" "+")) -> ("someone" "visits" "tiger" "+"))
The squirrel is red.
True
1
proof
[(triple2)]
("squirrel" "is" "red" "+")
triple2
The squirrel is not red.
False
1
inv-proof
[(triple2)]
("squirrel" "is" "red" "-")
triple2
The tiger visits the tiger.
True
2
proof
[(((triple3) -> rule3))]
("tiger" "visits" "tiger" "+")
((triple3) -> (rule3 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger does not visit the tiger.
False
2
inv-proof
[(((triple3) -> rule3))]
("tiger" "visits" "tiger" "-")
((triple3) -> (rule3 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger is cold.
True
3
proof
[(((((triple3) -> rule3)) -> rule1))]
("tiger" "is" "cold" "+")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
The tiger is not cold.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule1))]
("tiger" "is" "cold" "-")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
The squirrel is not cold.
Unknown
inv-rconc
[@2: The squirrel is cold.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("squirrel" "is" "cold" "-")
The squirrel visits the tiger.
Unknown
rconc
[@1: The squirrel visits the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "visits" "tiger" "+")
The dog is not cold.
Unknown
inv-rconc
[@1: The dog is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "is" "cold" "-")
The squirrel sees the dog.
Unknown
random
[@0: The squirrel sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "dog" "+")
The tiger is not round.
Unknown
inv-random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "-")
The dog likes the dog.
Unknown
random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "+")
@0: The dog does not visit the tiger.[(triple1)] The squirrel is red.[(triple2)] The tiger sees the squirrel.[(triple3)] @1: The tiger visits the tiger.[(((triple3) -> rule3))] @2: The tiger is cold.[(((((triple3) -> rule3)) -> rule1))]
The dog does not visit the tiger.
("dog" "visits" "tiger" "-")
triple1
The squirrel is red.
("squirrel" "is" "red" "+")
triple2
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
triple3
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
((triple3) -> (rule3 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2