Charlie is red. Dave is blue. Erin is red. Fiona is kind. If Charlie is red and Charlie is not round then Charlie is blue. If Erin is young and Erin is blue then Erin is kind. If someone is blue then they are kind. If Charlie is young and Charlie is not smart then Charlie is red. Kind people are not green. If someone is smart then they are red.
Charlie is red.
("Charlie" "is" "red" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Erin is red.
("Erin" "is" "red" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
If Charlie is red and Charlie is not round then Charlie is blue.
((("Charlie" "is" "red" "+") ("Charlie" "is" "round" "~")) -> ("Charlie" "is" "blue" "+"))
If Erin is young and Erin is blue then Erin is kind.
((("Erin" "is" "young" "+") ("Erin" "is" "blue" "+")) -> ("Erin" "is" "kind" "+"))
If someone is blue then they are kind.
((("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
If Charlie is young and Charlie is not smart then Charlie is red.
((("Charlie" "is" "young" "+") ("Charlie" "is" "smart" "~")) -> ("Charlie" "is" "red" "+"))
Kind people are not green.
((("someone" "is" "kind" "+")) -> ("someone" "is" "green" "-"))
If someone is smart then they are red.
((("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
Erin is red.
True
1
proof
[(triple3)]
("Erin" "is" "red" "+")
triple3
Charlie is not red.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "red" "-")
triple1
Fiona is not green.
True
2
proof
[(((triple4) -> rule5))]
("Fiona" "is" "green" "-")
((triple4) -> (rule5 % int1))
Fiona is not green.
("Fiona" "is" "green" "-")
int1
Dave is not kind.
False
2
inv-proof
[(((triple2) -> rule3))]
("Dave" "is" "kind" "-")
((triple2) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is not green.
True
3
proof
[(((((triple2) -> rule3)) -> rule5))]
("Dave" "is" "green" "-")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Dave is not green.
("Dave" "is" "green" "-")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is green.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule5))]
("Dave" "is" "green" "+")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Dave is not green.
("Dave" "is" "green" "-")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Charlie is not blue.
Unknown
inv-rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "blue" "-")
Fiona is red.
Unknown
rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "red" "+")
Erin is not kind.
Unknown
inv-rconc
[@1: Erin is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "kind" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
@0: Charlie is red.[(triple1)] Dave is blue.[(triple2)] Erin is red.[(triple3)] Fiona is kind.[(triple4)] @1: Dave is kind.[(((triple2) -> rule3))] Fiona is not green.[(((triple4) -> rule5))] @2: Dave is not green.[(((((triple2) -> rule3)) -> rule5))]
Charlie is red.
("Charlie" "is" "red" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
Erin is red.
("Erin" "is" "red" "+")
triple3
Fiona is kind.
("Fiona" "is" "kind" "+")
triple4
Dave is kind.
("Dave" "is" "kind" "+")
((triple2) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Fiona is not green.
("Fiona" "is" "green" "-")
((triple4) -> (rule5 % int1))
Fiona is not green.
("Fiona" "is" "green" "-")
int1
Dave is not green.
("Dave" "is" "green" "-")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Dave is not green.
("Dave" "is" "green" "-")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2