Anne is round. Charlie is big. Dave is quiet. Fiona is round. If something is rough then it is nice. If something is nice then it is blue. Big, quiet things are blue. If something is rough then it is blue. If Charlie is round and Charlie is white then Charlie is quiet. If something is white and nice then it is round. If Charlie is round then Charlie is blue. Big things are rough.
Anne is round.
("Anne" "is" "round" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Fiona is round.
("Fiona" "is" "round" "+")
If something is rough then it is nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
If something is nice then it is blue.
((("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
Big, quiet things are blue.
((("something" "is" "big" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
If something is rough then it is blue.
((("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
If Charlie is round and Charlie is white then Charlie is quiet.
((("Charlie" "is" "round" "+") ("Charlie" "is" "white" "+")) -> ("Charlie" "is" "quiet" "+"))
If something is white and nice then it is round.
((("something" "is" "white" "+") ("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
If Charlie is round then Charlie is blue.
((("Charlie" "is" "round" "+")) -> ("Charlie" "is" "blue" "+"))
Big things are rough.
((("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
Dave is quiet.
True
1
proof
[(triple3)]
("Dave" "is" "quiet" "+")
triple3
Dave is not quiet.
False
1
inv-proof
[(triple3)]
("Dave" "is" "quiet" "-")
triple3
Charlie is rough.
True
2
proof
[(((triple2) -> rule8))]
("Charlie" "is" "rough" "+")
((triple2) -> (rule8 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is not rough.
False
2
inv-proof
[(((triple2) -> rule8))]
("Charlie" "is" "rough" "-")
((triple2) -> (rule8 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is not round.
Unknown
inv-rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "round" "-")
Charlie is quiet.
Unknown
rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "quiet" "+")
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
@0: Anne is round.[(triple1)] Charlie is big.[(triple2)] Dave is quiet.[(triple3)] Fiona is round.[(triple4)] @1: Charlie is rough.[(((triple2) -> rule8))] @2: Charlie is blue.[(((((triple2) -> rule8)) -> rule4) OR ((((((triple2) -> rule8)) -> rule1)) -> rule2))] Charlie is nice.[(((((triple2) -> rule8)) -> rule1))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Charlie is big.
("Charlie" "is" "big" "+")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
Fiona is round.
("Fiona" "is" "round" "+")
triple4
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple2) -> (rule8 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((((triple2) -> (rule8 % int2))) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((((((triple2) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
((((triple2) -> (rule8 % int2))) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2