Anne is round. Charlie is big. Fiona is white. If something is rough and cold then it is round. If something is round and quiet then it is not rough. If Anne is cold and Anne is not white then Anne is not round. White things are big. If something is big then it is not quiet. If something is round and green then it is quiet.
Anne is round.
("Anne" "is" "round" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Fiona is white.
("Fiona" "is" "white" "+")
If something is rough and cold then it is round.
((("something" "is" "rough" "+") ("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
If something is round and quiet then it is not rough.
((("something" "is" "round" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "rough" "-"))
If Anne is cold and Anne is not white then Anne is not round.
((("Anne" "is" "cold" "+") ("Anne" "is" "white" "~")) -> ("Anne" "is" "round" "-"))
White things are big.
((("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
If something is big then it is not quiet.
((("something" "is" "big" "+")) -> ("something" "is" "quiet" "-"))
If something is round and green then it is quiet.
((("something" "is" "round" "+") ("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
Charlie is big.
True
1
proof
[(triple2)]
("Charlie" "is" "big" "+")
triple2
Anne is not round.
False
1
inv-proof
[(triple1)]
("Anne" "is" "round" "-")
triple1
Fiona is big.
True
2
proof
[(((triple3) -> rule4))]
("Fiona" "is" "big" "+")
((triple3) -> (rule4 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Charlie is quiet.
False
2
inv-proof
[(((triple2) -> rule5))]
("Charlie" "is" "quiet" "+")
((triple2) -> (rule5 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Fiona is not quiet.
True
3
proof
[(((((triple3) -> rule4)) -> rule5))]
("Fiona" "is" "quiet" "-")
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is quiet.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule5))]
("Fiona" "is" "quiet" "+")
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Anne is not quiet.
Unknown
inv-rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "quiet" "-")
Anne is big.
Unknown
rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "big" "+")
Fiona is not round.
Unknown
inv-rconc
[@1: Fiona is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "round" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
Anne is not white.
Unknown
inv-random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
@0: Anne is round.[(triple1)] Charlie is big.[(triple2)] Fiona is white.[(triple3)] @1: Charlie is not quiet.[(((triple2) -> rule5))] Fiona is big.[(((triple3) -> rule4))] @2: Fiona is not quiet.[(((((triple3) -> rule4)) -> rule5))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Charlie is big.
("Charlie" "is" "big" "+")
triple2
Fiona is white.
("Fiona" "is" "white" "+")
triple3
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
((triple2) -> (rule5 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((triple3) -> (rule4 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2