Charlie is red. Fiona is young. Gary is kind. Harry is blue. All young things are green. If something is red and quiet then it is kind. Kind things are cold. If something is quiet and red then it is green. All blue things are kind. If something is red and kind then it is cold.
Charlie is red.
("Charlie" "is" "red" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Harry is blue.
("Harry" "is" "blue" "+")
All young things are green.
((("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
If something is red and quiet then it is kind.
((("something" "is" "red" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
Kind things are cold.
((("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
If something is quiet and red then it is green.
((("something" "is" "quiet" "+") ("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
All blue things are kind.
((("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
If something is red and kind then it is cold.
((("something" "is" "red" "+") ("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
Gary is kind.
True
1
proof
[(triple3)]
("Gary" "is" "kind" "+")
triple3
Charlie is not red.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "red" "-")
triple1
Harry is kind.
True
2
proof
[(((triple4) -> rule5))]
("Harry" "is" "kind" "+")
((triple4) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is not kind.
False
2
inv-proof
[(((triple4) -> rule5))]
("Harry" "is" "kind" "-")
((triple4) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is cold.
True
3
proof
[(((((triple4) -> rule5)) -> rule3))]
("Harry" "is" "cold" "+")
((((triple4) -> (rule5 % int2))) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is not cold.
False
3
inv-proof
[(((((triple4) -> rule5)) -> rule3))]
("Harry" "is" "cold" "-")
((((triple4) -> (rule5 % int2))) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Charlie is not cold.
Unknown
inv-rconc
[@2: Charlie is cold.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Charlie" "is" "cold" "-")
Charlie is green.
Unknown
rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "green" "+")
Harry is not green.
Unknown
inv-rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "green" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
Harry is not young.
Unknown
inv-random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
@0: Charlie is red.[(triple1)] Fiona is young.[(triple2)] Gary is kind.[(triple3)] Harry is blue.[(triple4)] @1: Fiona is green.[(((triple2) -> rule1))] Gary is cold.[(((triple3) -> rule3))] Harry is kind.[(((triple4) -> rule5))] @2: Harry is cold.[(((((triple4) -> rule5)) -> rule3))]
Charlie is red.
("Charlie" "is" "red" "+")
triple1
Fiona is young.
("Fiona" "is" "young" "+")
triple2
Gary is kind.
("Gary" "is" "kind" "+")
triple3
Harry is blue.
("Harry" "is" "blue" "+")
triple4
Fiona is green.
("Fiona" "is" "green" "+")
((triple2) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((triple3) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((triple4) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((((triple4) -> (rule5 % int2))) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2