Anne is round. Bob is young. Charlie is quiet. If Charlie is white then Charlie is round. If someone is young then they are green. If someone is green then they are big.
Anne is round.
("Anne" "is" "round" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
If Charlie is white then Charlie is round.
((("Charlie" "is" "white" "+")) -> ("Charlie" "is" "round" "+"))
If someone is young then they are green.
((("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
If someone is green then they are big.
((("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
Bob is young.
True
1
proof
[(triple2)]
("Bob" "is" "young" "+")
triple2
Anne is not round.
False
1
inv-proof
[(triple1)]
("Anne" "is" "round" "-")
triple1
Bob is green.
True
2
proof
[(((triple2) -> rule2))]
("Bob" "is" "green" "+")
((triple2) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is not green.
False
2
inv-proof
[(((triple2) -> rule2))]
("Bob" "is" "green" "-")
((triple2) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is big.
True
3
proof
[(((((triple2) -> rule2)) -> rule3))]
("Bob" "is" "big" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is not big.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule3))]
("Bob" "is" "big" "-")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Charlie is not big.
Unknown
inv-rconc
[@2: Charlie is big.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Charlie" "is" "big" "-")
Charlie is round.
Unknown
rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "round" "+")
Charlie is not green.
Unknown
inv-rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "green" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
@0: Anne is round.[(triple1)] Bob is young.[(triple2)] Charlie is quiet.[(triple3)] @1: Bob is green.[(((triple2) -> rule2))] @2: Bob is big.[(((((triple2) -> rule2)) -> rule3))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Bob is young.
("Bob" "is" "young" "+")
triple2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Bob is green.
("Bob" "is" "green" "+")
((triple2) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2