Charlie is not quiet. Dave is blue. Erin is quiet. Fiona is red. If something is rough and not green then it is not round. Smart, red things are round. All red things are rough. If something is smart and not round then it is blue. If something is green and round then it is quiet. If something is rough and not blue then it is quiet.
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
Dave is blue.
("Dave" "is" "blue" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Fiona is red.
("Fiona" "is" "red" "+")
If something is rough and not green then it is not round.
((("something" "is" "rough" "+") ("something" "is" "green" "~")) -> ("something" "is" "round" "-"))
Smart, red things are round.
((("something" "is" "smart" "+") ("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
All red things are rough.
((("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
If something is smart and not round then it is blue.
((("something" "is" "smart" "+") ("something" "is" "round" "~")) -> ("something" "is" "blue" "+"))
If something is green and round then it is quiet.
((("something" "is" "green" "+") ("something" "is" "round" "+")) -> ("something" "is" "quiet" "+"))
If something is rough and not blue then it is quiet.
((("something" "is" "rough" "+") ("something" "is" "blue" "~")) -> ("something" "is" "quiet" "+"))
Charlie is not quiet.
True
1
proof
[(triple1)]
("Charlie" "is" "quiet" "-")
triple1
Charlie is quiet.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "quiet" "+")
triple1
Fiona is rough.
True
2
proof
[(((triple4) -> rule3))]
("Fiona" "is" "rough" "+")
((triple4) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is not rough.
False
2
inv-proof
[(((triple4) -> rule3))]
("Fiona" "is" "rough" "-")
((triple4) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Erin is not blue.
Unknown
inv-rconc
[@1: Erin is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "blue" "-")
Fiona is round.
Unknown
rconc
[@1: Fiona is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "round" "+")
Erin is not smart.
Unknown
inv-random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
@0: Charlie is not quiet.[(triple1)] Dave is blue.[(triple2)] Erin is quiet.[(triple3)] Fiona is red.[(triple4)] @1: Fiona is rough.[(((triple4) -> rule3))]
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
Erin is quiet.
("Erin" "is" "quiet" "+")
triple3
Fiona is red.
("Fiona" "is" "red" "+")
triple4
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple4) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1