Charlie is blue. Charlie is kind. Charlie is red. Fiona is red. Fiona is round. Fiona is not white. Harry is not red. If Charlie is nice and Charlie is not red then Charlie is not green. All green, round things are white. All kind things are not green. If Charlie is round and Charlie is red then Charlie is nice. Red, round things are blue. All kind things are blue.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is not white.
("Fiona" "is" "white" "-")
Harry is not red.
("Harry" "is" "red" "-")
If Charlie is nice and Charlie is not red then Charlie is not green.
((("Charlie" "is" "nice" "+") ("Charlie" "is" "red" "~")) -> ("Charlie" "is" "green" "-"))
All green, round things are white.
((("something" "is" "green" "+") ("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
All kind things are not green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "-"))
If Charlie is round and Charlie is red then Charlie is nice.
((("Charlie" "is" "round" "+") ("Charlie" "is" "red" "+")) -> ("Charlie" "is" "nice" "+"))
Red, round things are blue.
((("something" "is" "red" "+") ("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
All kind things are blue.
((("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
Harry is not red.
True
1
proof
[(triple7)]
("Harry" "is" "red" "-")
triple7
Fiona is white.
False
1
inv-proof
[(triple6)]
("Fiona" "is" "white" "+")
triple6
Fiona is blue.
True
3
proof
[(((triple4 triple5) -> rule5))]
("Fiona" "is" "blue" "+")
((triple4 triple5) -> (rule5 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Charlie is green.
False
2
inv-proof
[(((triple2) -> rule3))]
("Charlie" "is" "green" "+")
((triple2) -> (rule3 % int1))
Charlie is not green.
("Charlie" "is" "green" "-")
int1
Charlie is not white.
Unknown
inv-rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "white" "-")
Harry is blue.
Unknown
rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "blue" "+")
Fiona is not nice.
Unknown
inv-random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Charlie is blue.[(triple1 OR ((triple2) -> rule6))] Charlie is kind.[(triple2)] Charlie is red.[(triple3)] Fiona is not white.[(triple6)] Fiona is red.[(triple4)] Fiona is round.[(triple5)] Harry is not red.[(triple7)] @1: Charlie is not green.[(((triple2) -> rule3))] Fiona is blue.[(((triple4 triple5) -> rule5))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
((triple2) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Charlie is red.
("Charlie" "is" "red" "+")
triple3
Fiona is not white.
("Fiona" "is" "white" "-")
triple6
Fiona is red.
("Fiona" "is" "red" "+")
triple4
Fiona is round.
("Fiona" "is" "round" "+")
triple5
Harry is not red.
("Harry" "is" "red" "-")
triple7
Charlie is not green.
("Charlie" "is" "green" "-")
((triple2) -> (rule3 % int1))
Charlie is not green.
("Charlie" "is" "green" "-")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
((triple4 triple5) -> (rule5 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1