The cat is blue. Young things are cold. All round, kind things are young. If something is young then it is cold. If the cat is kind then the cat is round. If something is cold then it is round. Blue things are cold.
The cat is blue.
("cat" "is" "blue" "+")
Young things are cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
All round, kind things are young.
((("something" "is" "round" "+") ("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
If something is young then it is cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
If the cat is kind then the cat is round.
((("cat" "is" "kind" "+")) -> ("cat" "is" "round" "+"))
If something is cold then it is round.
((("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
Blue things are cold.
((("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
The cat is blue.
True
1
proof
[(triple1)]
("cat" "is" "blue" "+")
triple1
The cat is not blue.
False
1
inv-proof
[(triple1)]
("cat" "is" "blue" "-")
triple1
The cat is cold.
True
2
proof
[(((triple1) -> rule6))]
("cat" "is" "cold" "+")
((triple1) -> (rule6 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is not cold.
False
2
inv-proof
[(((triple1) -> rule6))]
("cat" "is" "cold" "-")
((triple1) -> (rule6 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is round.
True
3
proof
[(((((triple1) -> rule6)) -> rule5))]
("cat" "is" "round" "+")
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The cat is not round.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule5))]
("cat" "is" "round" "-")
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The cat is not young.
Unknown
inv-rconc
[@1: The cat is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "is" "young" "-")
The cat sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
The cat is not kind.
Unknown
inv-random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "-")
The cat chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
@0: The cat is blue.[(triple1)] @1: The cat is cold.[(((triple1) -> rule6))] @2: The cat is round.[(((((triple1) -> rule6)) -> rule5))]
The cat is blue.
("cat" "is" "blue" "+")
triple1
The cat is cold.
("cat" "is" "cold" "+")
((triple1) -> (rule6 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is round.
("cat" "is" "round" "+")
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2