Charlie is green. Dave is green. Gary is nice. Harry is not cold. If Harry is green then Harry is nice. All nice, red people are not furry. Cold people are red. Nice people are cold. Red people are cold. If Charlie is not nice and Charlie is not green then Charlie is cold.
Charlie is green.
("Charlie" "is" "green" "+")
Dave is green.
("Dave" "is" "green" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Harry is not cold.
("Harry" "is" "cold" "-")
If Harry is green then Harry is nice.
((("Harry" "is" "green" "+")) -> ("Harry" "is" "nice" "+"))
All nice, red people are not furry.
((("someone" "is" "nice" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "furry" "-"))
Cold people are red.
((("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
Nice people are cold.
((("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
Red people are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
If Charlie is not nice and Charlie is not green then Charlie is cold.
((("Charlie" "is" "nice" "~") ("Charlie" "is" "green" "~")) -> ("Charlie" "is" "cold" "+"))
Dave is green.
True
1
proof
[(triple2)]
("Dave" "is" "green" "+")
triple2
Gary is not nice.
False
1
inv-proof
[(triple3)]
("Gary" "is" "nice" "-")
triple3
Gary is cold.
True
2
proof
[(((triple3) -> rule4))]
("Gary" "is" "cold" "+")
((triple3) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is not cold.
False
2
inv-proof
[(((triple3) -> rule4))]
("Gary" "is" "cold" "-")
((triple3) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
True
3
proof
[(((((triple3) -> rule4)) -> rule3))]
("Gary" "is" "red" "+")
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is not red.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule3))]
("Gary" "is" "red" "-")
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is not furry.
True
5
proof
[(((triple3 ((((triple3) -> rule4)) -> rule3)) -> rule2))]
("Gary" "is" "furry" "-")
((triple3 ((((triple3) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Gary is not furry.
("Gary" "is" "furry" "-")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is furry.
False
5
inv-proof
[(((triple3 ((((triple3) -> rule4)) -> rule3)) -> rule2))]
("Gary" "is" "furry" "+")
((triple3 ((((triple3) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Gary is not furry.
("Gary" "is" "furry" "-")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Dave is not cold.
Unknown
inv-rconc
[@3: Dave is cold.[CWA. Example of deepest failure = (rule5 <- rule3 <- rule4 <- FAIL)]]
("Dave" "is" "cold" "-")
Charlie is cold.
Unknown
rconc
[@3: Charlie is cold.[CWA. Example of deepest failure = (rule5 <- rule3 <- rule4 <- FAIL)]]
("Charlie" "is" "cold" "+")
Harry is not red.
Unknown
inv-rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "red" "-")
Harry is nice.
Unknown
rconc
[@1: Harry is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "nice" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Charlie is green.[(triple1)] Dave is green.[(triple2)] Gary is nice.[(triple3)] Harry is not cold.[(triple4)] @1: Gary is cold.[(((triple3) -> rule4))] @2: Gary is red.[(((((triple3) -> rule4)) -> rule3))] @3: Gary is not furry.[(((triple3 ((((triple3) -> rule4)) -> rule3)) -> rule2))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
Gary is nice.
("Gary" "is" "nice" "+")
triple3
Harry is not cold.
("Harry" "is" "cold" "-")
triple4
Gary is cold.
("Gary" "is" "cold" "+")
((triple3) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is not furry.
("Gary" "is" "furry" "-")
((triple3 ((((triple3) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Gary is not furry.
("Gary" "is" "furry" "-")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3