Dave is not rough. Gary is young. Cold people are round. If someone is young then they are cold. Cold people are young. If Gary is not kind then Gary is young. If Gary is cold and Gary is round then Gary is not rough. If Gary is not young then Gary is not round.
Dave is not rough.
("Dave" "is" "rough" "-")
Gary is young.
("Gary" "is" "young" "+")
Cold people are round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
If someone is young then they are cold.
((("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
Cold people are young.
((("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
If Gary is not kind then Gary is young.
((("Gary" "is" "kind" "~")) -> ("Gary" "is" "young" "+"))
If Gary is cold and Gary is round then Gary is not rough.
((("Gary" "is" "cold" "+") ("Gary" "is" "round" "+")) -> ("Gary" "is" "rough" "-"))
If Gary is not young then Gary is not round.
((("Gary" "is" "young" "~")) -> ("Gary" "is" "round" "-"))
Dave is not rough.
True
1
proof
[(triple1)]
("Dave" "is" "rough" "-")
triple1
Gary is not young.
False
1
inv-proof
[(triple2)]
("Gary" "is" "young" "-")
triple2
Gary is cold.
True
2
proof
[(((triple2) -> rule2))]
("Gary" "is" "cold" "+")
((triple2) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is not cold.
False
2
inv-proof
[(((triple2) -> rule2))]
("Gary" "is" "cold" "-")
((triple2) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is round.
True
3
proof
[(((((triple2) -> rule2)) -> rule1))]
("Gary" "is" "round" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is not round.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule1))]
("Gary" "is" "round" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is not rough.
True
6
proof
[(((((triple2) -> rule2) ((((triple2) -> rule2)) -> rule1)) -> rule5))]
("Gary" "is" "rough" "-")
((((triple2) -> (rule2 % int3)) ((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is rough.
False
6
inv-proof
[(((((triple2) -> rule2) ((((triple2) -> rule2)) -> rule1)) -> rule5))]
("Gary" "is" "rough" "+")
((((triple2) -> (rule2 % int3)) ((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Dave is not round.
Unknown
inv-rconc
[@3: Dave is round.[CWA. Example of deepest failure = (rule1 <- rule2 <- rule3 <- FAIL)]]
("Dave" "is" "round" "-")
Dave is cold.
Unknown
rconc
[@2: Dave is cold.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Dave" "is" "cold" "+")
Dave is not young.
Unknown
inv-rconc
[@2: Dave is young.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Dave" "is" "young" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
Gary is not white.
Unknown
inv-random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
@0: Dave is not rough.[(triple1)] Gary is young.[(triple2)] @1: Gary is cold.[(((triple2) -> rule2))] @2: Gary is round.[(((((triple2) -> rule2)) -> rule1))] @3: Gary is not rough.[(((((triple2) -> rule2) ((((triple2) -> rule2)) -> rule1)) -> rule5))]
Dave is not rough.
("Dave" "is" "rough" "-")
triple1
Gary is young.
("Gary" "is" "young" "+")
triple2
Gary is cold.
("Gary" "is" "cold" "+")
((triple2) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is not rough.
("Gary" "is" "rough" "-")
((((triple2) -> (rule2 % int3)) ((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3