Anne is cold. Gary is cold. Harry is furry. Red, kind things are young. If something is kind and not blue then it is young. If Anne is not furry then Anne is kind. All young things are red. All blue things are red. All red, young things are rough. If something is kind then it is rough. If Gary is cold then Gary is young.
Anne is cold.
("Anne" "is" "cold" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Red, kind things are young.
((("something" "is" "red" "+") ("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
If something is kind and not blue then it is young.
((("something" "is" "kind" "+") ("something" "is" "blue" "~")) -> ("something" "is" "young" "+"))
If Anne is not furry then Anne is kind.
((("Anne" "is" "furry" "~")) -> ("Anne" "is" "kind" "+"))
All young things are red.
((("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
All blue things are red.
((("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
All red, young things are rough.
((("something" "is" "red" "+") ("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
If something is kind then it is rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
If Gary is cold then Gary is young.
((("Gary" "is" "cold" "+")) -> ("Gary" "is" "young" "+"))
Gary is cold.
True
1
proof
[(triple2)]
("Gary" "is" "cold" "+")
triple2
Gary is not cold.
False
1
inv-proof
[(triple2)]
("Gary" "is" "cold" "-")
triple2
Gary is young.
True
2
proof
[(((triple2) -> rule8))]
("Gary" "is" "young" "+")
((triple2) -> (rule8 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is not young.
False
2
inv-proof
[(((triple2) -> rule8))]
("Gary" "is" "young" "-")
((triple2) -> (rule8 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is red.
True
3
proof
[(((((triple2) -> rule8)) -> rule4))]
("Gary" "is" "red" "+")
((((triple2) -> (rule8 % int2))) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is not red.
False
3
inv-proof
[(((((triple2) -> rule8)) -> rule4))]
("Gary" "is" "red" "-")
((((triple2) -> (rule8 % int2))) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is rough.
True
6
proof
[(((((((triple2) -> rule8)) -> rule4) ((triple2) -> rule8)) -> rule6))]
("Gary" "is" "rough" "+")
((((((triple2) -> (rule8 % int3))) -> (rule4 % int2)) ((triple2) -> (rule8 % int3))) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is not rough.
False
6
inv-proof
[(((((((triple2) -> rule8)) -> rule4) ((triple2) -> rule8)) -> rule6))]
("Gary" "is" "rough" "-")
((((((triple2) -> (rule8 % int3))) -> (rule4 % int2)) ((triple2) -> (rule8 % int3))) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Anne is not rough.
Unknown
inv-rconc
[@3: Anne is rough.[CWA. Example of deepest failure = (rule6 <- rule1 <- rule3 <- FAIL)]]
("Anne" "is" "rough" "-")
Anne is young.
Unknown
rconc
[@2: Anne is young.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Anne" "is" "young" "+")
Anne is not kind.
Unknown
inv-rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "kind" "-")
Harry is young.
Unknown
rconc
[@1: Harry is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "young" "+")
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
@0: Anne is cold.[(triple1)] Gary is cold.[(triple2)] Harry is furry.[(triple3)] @1: Gary is young.[(((triple2) -> rule8))] @2: Gary is red.[(((((triple2) -> rule8)) -> rule4))] @3: Gary is rough.[(((((((triple2) -> rule8)) -> rule4) ((triple2) -> rule8)) -> rule6))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Gary is cold.
("Gary" "is" "cold" "+")
triple2
Harry is furry.
("Harry" "is" "furry" "+")
triple3
Gary is young.
("Gary" "is" "young" "+")
((triple2) -> (rule8 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((((triple2) -> (rule8 % int2))) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
((((((triple2) -> (rule8 % int3))) -> (rule4 % int2)) ((triple2) -> (rule8 % int3))) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3