Anne is furry. Bob is not round. Fiona is rough. Harry is blue. If someone is round then they are blue. If Bob is blue and Bob is furry then Bob is not white. Rough people are round. If Anne is red then Anne is quiet. If someone is blue then they are quiet. If Harry is rough and Harry is not blue then Harry is not red.
Anne is furry.
("Anne" "is" "furry" "+")
Bob is not round.
("Bob" "is" "round" "-")
Fiona is rough.
("Fiona" "is" "rough" "+")
Harry is blue.
("Harry" "is" "blue" "+")
If someone is round then they are blue.
((("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
If Bob is blue and Bob is furry then Bob is not white.
((("Bob" "is" "blue" "+") ("Bob" "is" "furry" "+")) -> ("Bob" "is" "white" "-"))
Rough people are round.
((("someone" "is" "rough" "+")) -> ("someone" "is" "round" "+"))
If Anne is red then Anne is quiet.
((("Anne" "is" "red" "+")) -> ("Anne" "is" "quiet" "+"))
If someone is blue then they are quiet.
((("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
If Harry is rough and Harry is not blue then Harry is not red.
((("Harry" "is" "rough" "+") ("Harry" "is" "blue" "~")) -> ("Harry" "is" "red" "-"))
Fiona is rough.
True
1
proof
[(triple3)]
("Fiona" "is" "rough" "+")
triple3
Fiona is not rough.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "rough" "-")
triple3
Fiona is round.
True
2
proof
[(((triple3) -> rule3))]
("Fiona" "is" "round" "+")
((triple3) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Harry is not quiet.
False
2
inv-proof
[(((triple4) -> rule5))]
("Harry" "is" "quiet" "-")
((triple4) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Fiona is blue.
True
3
proof
[(((((triple3) -> rule3)) -> rule1))]
("Fiona" "is" "blue" "+")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is not blue.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule1))]
("Fiona" "is" "blue" "-")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is quiet.
True
4
proof
[(((((((triple3) -> rule3)) -> rule1)) -> rule5))]
("Fiona" "is" "quiet" "+")
((((((triple3) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is not quiet.
False
4
inv-proof
[(((((((triple3) -> rule3)) -> rule1)) -> rule5))]
("Fiona" "is" "quiet" "-")
((((((triple3) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Anne is not quiet.
Unknown
inv-rconc
[@3: Anne is quiet.[CWA. Example of deepest failure = (rule5 <- rule1 <- rule3 <- FAIL)]]
("Anne" "is" "quiet" "-")
Bob is blue.
Unknown
rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "blue" "+")
Anne is not blue.
Unknown
inv-rconc
[@2: Anne is blue.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Anne" "is" "blue" "-")
Bob is quiet.
Unknown
rconc
[@2: Bob is quiet.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Bob" "is" "quiet" "+")
Fiona is not white.
Unknown
inv-random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
Fiona is not red.
Unknown
inv-random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
@0: Anne is furry.[(triple1)] Bob is not round.[(triple2)] Fiona is rough.[(triple3)] Harry is blue.[(triple4)] @1: Fiona is round.[(((triple3) -> rule3))] Harry is quiet.[(((triple4) -> rule5))] @2: Fiona is blue.[(((((triple3) -> rule3)) -> rule1))] @3: Fiona is quiet.[(((((((triple3) -> rule3)) -> rule1)) -> rule5))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Bob is not round.
("Bob" "is" "round" "-")
triple2
Fiona is rough.
("Fiona" "is" "rough" "+")
triple3
Harry is blue.
("Harry" "is" "blue" "+")
triple4
Fiona is round.
("Fiona" "is" "round" "+")
((triple3) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple4) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((((((triple3) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3