Anne is quiet. Bob is rough. Charlie is smart. Harry is rough. If Harry is quiet and Harry is rough then Harry is smart. If Anne is round then Anne is rough. White things are round. Quiet, young things are white. All smart things are rough. If something is quiet then it is white.
Anne is quiet.
("Anne" "is" "quiet" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If Harry is quiet and Harry is rough then Harry is smart.
((("Harry" "is" "quiet" "+") ("Harry" "is" "rough" "+")) -> ("Harry" "is" "smart" "+"))
If Anne is round then Anne is rough.
((("Anne" "is" "round" "+")) -> ("Anne" "is" "rough" "+"))
White things are round.
((("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
Quiet, young things are white.
((("something" "is" "quiet" "+") ("something" "is" "young" "+")) -> ("something" "is" "white" "+"))
All smart things are rough.
((("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
If something is quiet then it is white.
((("something" "is" "quiet" "+")) -> ("something" "is" "white" "+"))
Bob is rough.
True
1
proof
[(triple2)]
("Bob" "is" "rough" "+")
triple2
Bob is not rough.
False
1
inv-proof
[(triple2)]
("Bob" "is" "rough" "-")
triple2
Charlie is rough.
True
2
proof
[(((triple3) -> rule5))]
("Charlie" "is" "rough" "+")
((triple3) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is not rough.
False
2
inv-proof
[(((triple3) -> rule5))]
("Charlie" "is" "rough" "-")
((triple3) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Anne is round.
True
3
proof
[(((((triple1) -> rule6)) -> rule3))]
("Anne" "is" "round" "+")
((((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is not round.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule3))]
("Anne" "is" "round" "-")
((((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Harry is not round.
Unknown
inv-rconc
[@2: Harry is round.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("Harry" "is" "round" "-")
Bob is round.
Unknown
rconc
[@2: Bob is round.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("Bob" "is" "round" "+")
Charlie is not round.
Unknown
inv-rconc
[@2: Charlie is round.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("Charlie" "is" "round" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
Anne is not young.
Unknown
inv-random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
@0: Anne is quiet.[(triple1)] Bob is rough.[(triple2)] Charlie is smart.[(triple3)] Harry is rough.[(triple4)] @1: Anne is white.[(((triple1) -> rule6))] Charlie is rough.[(((triple3) -> rule5))] @2: Anne is round.[(((((triple1) -> rule6)) -> rule3))] @3: Anne is rough.[(((((((triple1) -> rule6)) -> rule3)) -> rule2))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple3
Harry is rough.
("Harry" "is" "rough" "+")
triple4
Anne is white.
("Anne" "is" "white" "+")
((triple1) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple3) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
((((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
((((((triple1) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3