Anne is quiet. Bob is round. Charlie is red. Erin is smart. All quiet things are round. If Anne is smart and Anne is not nice then Anne is not quiet.
Anne is quiet.
("Anne" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Erin is smart.
("Erin" "is" "smart" "+")
All quiet things are round.
((("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
If Anne is smart and Anne is not nice then Anne is not quiet.
((("Anne" "is" "smart" "+") ("Anne" "is" "nice" "~")) -> ("Anne" "is" "quiet" "-"))
Erin is smart.
True
1
proof
[(triple4)]
("Erin" "is" "smart" "+")
triple4
Charlie is not red.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "red" "-")
triple3
Anne is round.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "round" "+")
((triple1) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is not round.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "round" "-")
((triple1) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Charlie is not round.
Unknown
inv-rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "round" "-")
Erin is round.
Unknown
rconc
[@1: Erin is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "round" "+")
Erin is not green.
Unknown
inv-random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
@0: Anne is quiet.[(triple1)] Bob is round.[(triple2)] Charlie is red.[(triple3)] Erin is smart.[(triple4)] @1: Anne is round.[(((triple1) -> rule1))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
Charlie is red.
("Charlie" "is" "red" "+")
triple3
Erin is smart.
("Erin" "is" "smart" "+")
triple4
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1