Charlie is not nice. Dave is kind. Erin is kind. Fiona is round. Quiet people are nice. If someone is blue then they are not nice. Quiet people are not blue. Kind people are blue. If Charlie is round and Charlie is cold then Charlie is blue. If someone is blue then they are cold. If someone is nice and cold then they are white. All round people are white.
Charlie is not nice.
("Charlie" "is" "nice" "-")
Dave is kind.
("Dave" "is" "kind" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Quiet people are nice.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
If someone is blue then they are not nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "-"))
Quiet people are not blue.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "-"))
Kind people are blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
If Charlie is round and Charlie is cold then Charlie is blue.
((("Charlie" "is" "round" "+") ("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "blue" "+"))
If someone is blue then they are cold.
((("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
If someone is nice and cold then they are white.
((("someone" "is" "nice" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
All round people are white.
((("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
Fiona is round.
True
1
proof
[(triple4)]
("Fiona" "is" "round" "+")
triple4
Erin is not kind.
False
1
inv-proof
[(triple3)]
("Erin" "is" "kind" "-")
triple3
Fiona is white.
True
2
proof
[(((triple4) -> rule8))]
("Fiona" "is" "white" "+")
((triple4) -> (rule8 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Erin is not blue.
False
2
inv-proof
[(((triple3) -> rule4))]
("Erin" "is" "blue" "-")
((triple3) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Fiona is not nice.
Unknown
inv-rconc
[@1: Fiona is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "nice" "-")
Dave is white.
Unknown
rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Dave" "is" "white" "+")
Fiona is not quiet.
Unknown
inv-random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
@0: Charlie is not nice.[(triple1)] Dave is kind.[(triple2)] Erin is kind.[(triple3)] Fiona is round.[(triple4)] @1: Dave is blue.[(((triple2) -> rule4))] Erin is blue.[(((triple3) -> rule4))] Fiona is white.[(((triple4) -> rule8))] @2: Dave is cold.[(((((triple2) -> rule4)) -> rule6))] Dave is not nice.[(((((triple2) -> rule4)) -> rule2))] Erin is cold.[(((((triple3) -> rule4)) -> rule6))] Erin is not nice.[(((((triple3) -> rule4)) -> rule2))]
Charlie is not nice.
("Charlie" "is" "nice" "-")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Erin is kind.
("Erin" "is" "kind" "+")
triple3
Fiona is round.
("Fiona" "is" "round" "+")
triple4
Dave is blue.
("Dave" "is" "blue" "+")
((triple2) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple3) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
((triple4) -> (rule8 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is not nice.
("Dave" "is" "nice" "-")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is not nice.
("Erin" "is" "nice" "-")
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
Erin is not nice.
("Erin" "is" "nice" "-")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2