Anne is round. Erin is green. Gary is quiet. Harry is kind. If Erin is white then Erin is green. If something is white and green then it is round. Green things are round. Nice, quiet things are kind. If something is nice then it is rough. If Anne is rough then Anne is quiet. Round, nice things are rough. All round things are rough.
Anne is round.
("Anne" "is" "round" "+")
Erin is green.
("Erin" "is" "green" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Harry is kind.
("Harry" "is" "kind" "+")
If Erin is white then Erin is green.
((("Erin" "is" "white" "+")) -> ("Erin" "is" "green" "+"))
If something is white and green then it is round.
((("something" "is" "white" "+") ("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
Green things are round.
((("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
Nice, quiet things are kind.
((("something" "is" "nice" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
If something is nice then it is rough.
((("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
If Anne is rough then Anne is quiet.
((("Anne" "is" "rough" "+")) -> ("Anne" "is" "quiet" "+"))
Round, nice things are rough.
((("something" "is" "round" "+") ("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
All round things are rough.
((("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
Anne is round.
True
1
proof
[(triple1)]
("Anne" "is" "round" "+")
triple1
Gary is not quiet.
False
1
inv-proof
[(triple3)]
("Gary" "is" "quiet" "-")
triple3
Erin is round.
True
2
proof
[(((triple2) -> rule3))]
("Erin" "is" "round" "+")
((triple2) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is not round.
False
2
inv-proof
[(((triple2) -> rule3))]
("Erin" "is" "round" "-")
((triple2) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Anne is quiet.
True
3
proof
[(((((triple1) -> rule8)) -> rule6))]
("Anne" "is" "quiet" "+")
((((triple1) -> (rule8 % int2))) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Erin is not rough.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule8))]
("Erin" "is" "rough" "-")
((((triple2) -> (rule3 % int2))) -> (rule8 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Anne is not kind.
Unknown
inv-rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "kind" "-")
Harry is round.
Unknown
rconc
[@1: Harry is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "round" "+")
Harry is not rough.
Unknown
inv-rconc
[@2: Harry is rough.[CWA. Example of deepest failure = (rule8 <- rule2 <- FAIL)]]
("Harry" "is" "rough" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
Erin is not nice.
Unknown
inv-random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
@0: Anne is round.[(triple1)] Erin is green.[(triple2)] Gary is quiet.[(triple3)] Harry is kind.[(triple4)] @1: Anne is rough.[(((triple1) -> rule8))] Erin is round.[(((triple2) -> rule3))] @2: Anne is quiet.[(((((triple1) -> rule8)) -> rule6))] Erin is rough.[(((((triple2) -> rule3)) -> rule8))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Erin is green.
("Erin" "is" "green" "+")
triple2
Gary is quiet.
("Gary" "is" "quiet" "+")
triple3
Harry is kind.
("Harry" "is" "kind" "+")
triple4
Anne is rough.
("Anne" "is" "rough" "+")
((triple1) -> (rule8 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
((triple2) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
((((triple1) -> (rule8 % int2))) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((((triple2) -> (rule3 % int2))) -> (rule8 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2