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