Charlie is red. Fiona is not kind. Harry is cold. Kind things are green. Red things are green. If something is red and nice then it is not round. If something is red and not cold then it is not round. Cold, green things are round. Nice things are not round. All kind, nice things are round. Green things are not kind.
Charlie is red.
("Charlie" "is" "red" "+")
Fiona is not kind.
("Fiona" "is" "kind" "-")
Harry is cold.
("Harry" "is" "cold" "+")
Kind things are green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
Red things are green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
If something is red and nice then it is not round.
((("something" "is" "red" "+") ("something" "is" "nice" "+")) -> ("something" "is" "round" "-"))
If something is red and not cold then it is not round.
((("something" "is" "red" "+") ("something" "is" "cold" "~")) -> ("something" "is" "round" "-"))
Cold, green things are round.
((("something" "is" "cold" "+") ("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
Nice things are not round.
((("something" "is" "nice" "+")) -> ("something" "is" "round" "-"))
All kind, nice things are round.
((("something" "is" "kind" "+") ("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
Green things are not kind.
((("something" "is" "green" "+")) -> ("something" "is" "kind" "-"))
Charlie is red.
True
1
proof
[(triple1)]
("Charlie" "is" "red" "+")
triple1
Charlie is not red.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "red" "-")
triple1
Charlie is green.
True
2
proof
[(((triple1) -> rule2))]
("Charlie" "is" "green" "+")
((triple1) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is not green.
False
2
inv-proof
[(((triple1) -> rule2))]
("Charlie" "is" "green" "-")
((triple1) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is not kind.
True
3
proof
[(((((triple1) -> rule2)) -> rule8))]
("Charlie" "is" "kind" "-")
((((triple1) -> (rule2 % int2))) -> (rule8 % int1))
Charlie is not kind.
("Charlie" "is" "kind" "-")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is kind.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule8))]
("Charlie" "is" "kind" "+")
((((triple1) -> (rule2 % int2))) -> (rule8 % int1))
Charlie is not kind.
("Charlie" "is" "kind" "-")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Harry is not green.
Unknown
inv-rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "green" "-")
Charlie is round.
Unknown
rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "round" "+")
Harry is not round.
Unknown
inv-rconc
[@2: Harry is round.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Harry" "is" "round" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
Harry is not nice.
Unknown
inv-random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
@0: Charlie is red.[(triple1)] Fiona is not kind.[(triple2)] Harry is cold.[(triple3)] @1: Charlie is green.[(((triple1) -> rule2))] @2: Charlie is not kind.[(((((triple1) -> rule2)) -> rule8))]
Charlie is red.
("Charlie" "is" "red" "+")
triple1
Fiona is not kind.
("Fiona" "is" "kind" "-")
triple2
Harry is cold.
("Harry" "is" "cold" "+")
triple3
Charlie is green.
("Charlie" "is" "green" "+")
((triple1) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is not kind.
("Charlie" "is" "kind" "-")
((((triple1) -> (rule2 % int2))) -> (rule8 % int1))
Charlie is not kind.
("Charlie" "is" "kind" "-")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2