Charlie is not quiet. Dave is rough. Erin is not quiet. If Charlie is big and Charlie is not smart then Charlie is blue. Quiet, cold things are big. All rough, cold things are not big. Rough things are quiet. All smart, big things are green. If something is blue and not cold then it is not rough. All quiet things are blue. If Erin is not cold then Erin is blue.
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
Dave is rough.
("Dave" "is" "rough" "+")
Erin is not quiet.
("Erin" "is" "quiet" "-")
If Charlie is big and Charlie is not smart then Charlie is blue.
((("Charlie" "is" "big" "+") ("Charlie" "is" "smart" "~")) -> ("Charlie" "is" "blue" "+"))
Quiet, cold things are big.
((("something" "is" "quiet" "+") ("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
All rough, cold things are not big.
((("something" "is" "rough" "+") ("something" "is" "cold" "+")) -> ("something" "is" "big" "-"))
Rough things are quiet.
((("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
All smart, big things are green.
((("something" "is" "smart" "+") ("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
If something is blue and not cold then it is not rough.
((("something" "is" "blue" "+") ("something" "is" "cold" "~")) -> ("something" "is" "rough" "-"))
All quiet things are blue.
((("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
If Erin is not cold then Erin is blue.
((("Erin" "is" "cold" "~")) -> ("Erin" "is" "blue" "+"))
Erin is not quiet.
True
1
proof
[(triple3)]
("Erin" "is" "quiet" "-")
triple3
Dave is not rough.
False
1
inv-proof
[(triple2)]
("Dave" "is" "rough" "-")
triple2
Erin is not green.
Unknown
inv-rconc
[@1: Erin is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "green" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
@0: Charlie is not quiet.[(triple1)] Dave is rough.[(triple2)] Erin is not quiet.[(triple3)] @1: Dave is quiet.[(((triple2) -> rule4))] @2: Dave is blue.[(((((triple2) -> rule4)) -> rule7))]
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
triple1
Dave is rough.
("Dave" "is" "rough" "+")
triple2
Erin is not quiet.
("Erin" "is" "quiet" "-")
triple3
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple2) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((((triple2) -> (rule4 % int2))) -> (rule7 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2