Anne is quiet. Fiona is not round. Fiona is white. If Anne is round then Anne is quiet. If something is furry and not white then it is not red. All white things are red. If something is smart then it is not nice. If something is quiet and not white then it is not nice. Nice things are smart. Red things are not quiet. If something is nice and not white then it is not round.
Anne is quiet.
("Anne" "is" "quiet" "+")
Fiona is not round.
("Fiona" "is" "round" "-")
Fiona is white.
("Fiona" "is" "white" "+")
If Anne is round then Anne is quiet.
((("Anne" "is" "round" "+")) -> ("Anne" "is" "quiet" "+"))
If something is furry and not white then it is not red.
((("something" "is" "furry" "+") ("something" "is" "white" "~")) -> ("something" "is" "red" "-"))
All white things are red.
((("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
If something is smart then it is not nice.
((("something" "is" "smart" "+")) -> ("something" "is" "nice" "-"))
If something is quiet and not white then it is not nice.
((("something" "is" "quiet" "+") ("something" "is" "white" "~")) -> ("something" "is" "nice" "-"))
Nice things are smart.
((("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
Red things are not quiet.
((("something" "is" "red" "+")) -> ("something" "is" "quiet" "-"))
If something is nice and not white then it is not round.
((("something" "is" "nice" "+") ("something" "is" "white" "~")) -> ("something" "is" "round" "-"))
Fiona is not round.
True
1
proof
[(triple2)]
("Fiona" "is" "round" "-")
triple2
Anne is not quiet.
False
1
inv-proof
[(triple1)]
("Anne" "is" "quiet" "-")
triple1
Fiona is red.
True
2
proof
[(((triple3) -> rule3))]
("Fiona" "is" "red" "+")
((triple3) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is not red.
False
2
inv-proof
[(((triple3) -> rule3))]
("Fiona" "is" "red" "-")
((triple3) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is not quiet.
True
3
proof
[(((((triple3) -> rule3)) -> rule7))]
("Fiona" "is" "quiet" "-")
((((triple3) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is quiet.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule7))]
("Fiona" "is" "quiet" "+")
((((triple3) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is not smart.
Unknown
inv-rconc
[@1: Fiona is smart.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "smart" "-")
Anne is smart.
Unknown
rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "smart" "+")
Anne is not red.
Unknown
inv-rconc
[@1: Anne is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "red" "-")
Fiona is furry.
Unknown
random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "+")
Anne is not round.
Unknown
inv-random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
@0: Anne is quiet.[(triple1)] Fiona is not round.[(triple2)] Fiona is white.[(triple3)] @1: Fiona is red.[(((triple3) -> rule3))] @2: Fiona is not quiet.[(((((triple3) -> rule3)) -> rule7))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Fiona is not round.
("Fiona" "is" "round" "-")
triple2
Fiona is white.
("Fiona" "is" "white" "+")
triple3
Fiona is red.
("Fiona" "is" "red" "+")
((triple3) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
((((triple3) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2