Anne is blue. Anne is green. Anne is rough. Charlie is quiet. Dave is young. Fiona is quiet. Fiona is white. Quiet, young people are rough. If someone is blue then they are quiet. If someone is white and furry then they are rough. If someone is young then they are white. If someone is quiet then they are furry. Furry people are blue. All green, furry people are white. All furry, rough people are young.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Quiet, young people are rough.
((("someone" "is" "quiet" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
If someone is blue then they are quiet.
((("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
If someone is white and furry then they are rough.
((("someone" "is" "white" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
If someone is young then they are white.
((("someone" "is" "young" "+")) -> ("someone" "is" "white" "+"))
If someone is quiet then they are furry.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "furry" "+"))
Furry people are blue.
((("someone" "is" "furry" "+")) -> ("someone" "is" "blue" "+"))
All green, furry people are white.
((("someone" "is" "green" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
All furry, rough people are young.
((("someone" "is" "furry" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
Dave is young.
True
1
proof
[(triple5)]
("Dave" "is" "young" "+")
triple5
Fiona is not white.
False
1
inv-proof
[(triple7)]
("Fiona" "is" "white" "-")
triple7
Charlie is furry.
True
2
proof
[(((triple4) -> rule5))]
("Charlie" "is" "furry" "+")
((triple4) -> (rule5 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Fiona is not furry.
False
2
inv-proof
[(((triple6) -> rule5))]
("Fiona" "is" "furry" "-")
((triple6) -> (rule5 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Anne is furry.
True
3
proof
[(((((triple1) -> rule2)) -> rule5))]
("Anne" "is" "furry" "+")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Fiona is not blue.
False
3
inv-proof
[(((((triple6) -> rule5)) -> rule6))]
("Fiona" "is" "blue" "-")
((((triple6) -> (rule5 % int2))) -> (rule6 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Anne is white.
True
5
proof
[(((triple2 ((((triple1) -> rule2)) -> rule5)) -> rule7) OR ((((((((triple1) -> rule2)) -> rule5) triple3) -> rule8)) -> rule4))]
("Anne" "is" "white" "+")
((triple2 ((((triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
((((((((triple1) -> (rule2 % int4))) -> (rule5 % int3)) triple3) -> (rule8 % int2))) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
int4
Anne is not white.
False
5
inv-proof
[(((triple2 ((((triple1) -> rule2)) -> rule5)) -> rule7) OR ((((((((triple1) -> rule2)) -> rule5) triple3) -> rule8)) -> rule4))]
("Anne" "is" "white" "-")
((triple2 ((((triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
((((((((triple1) -> (rule2 % int4))) -> (rule5 % int3)) triple3) -> (rule8 % int2))) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
int4
Dave is not rough.
Unknown
inv-rconc
[@4: Dave is rough.[CWA. Example of deepest failure = (rule1 <- rule2 <- rule6 <- rule5 <- FAIL)]]
("Dave" "is" "rough" "-")
Dave is blue.
Unknown
rconc
[@3: Dave is blue.[CWA. Example of deepest failure = (rule6 <- rule5 <- rule2 <- FAIL)]]
("Dave" "is" "blue" "+")
Charlie is not young.
Unknown
inv-rconc
[@3: Charlie is young.[CWA. Example of deepest failure = (rule8 <- rule3 <- rule4 <- FAIL)]]
("Charlie" "is" "young" "-")
Charlie is rough.
Unknown
rconc
[@4: Charlie is rough.[CWA. Example of deepest failure = (rule1 <- rule8 <- rule3 <- rule4 <- FAIL)]]
("Charlie" "is" "rough" "+")
Dave is not green.
Unknown
inv-random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "-")
Fiona is green.
Unknown
random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "+")
@0: Anne is blue.[(triple1)] Anne is green.[(triple2)] Anne is rough.[(triple3 OR ((((triple2 ((((triple1) -> rule2)) -> rule5)) -> rule7) ((((triple1) -> rule2)) -> rule5)) -> rule3))] Charlie is quiet.[(triple4)] Dave is young.[(triple5)] Fiona is quiet.[(triple6)] Fiona is white.[(triple7)] @1: Anne is quiet.[(((triple1) -> rule2))] Charlie is furry.[(((triple4) -> rule5))] Dave is white.[(((triple5) -> rule4))] Fiona is furry.[(((triple6) -> rule5))] @2: Anne is furry.[(((((triple1) -> rule2)) -> rule5))] Charlie is blue.[(((((triple4) -> rule5)) -> rule6))] Fiona is blue.[(((((triple6) -> rule5)) -> rule6))] Fiona is rough.[(((triple7 ((triple6) -> rule5)) -> rule3))] @3: Anne is white.[(((triple2 ((((triple1) -> rule2)) -> rule5)) -> rule7) OR ((((((((triple1) -> rule2)) -> rule5) triple3) -> rule8)) -> rule4))] Anne is young.[(((((((triple1) -> rule2)) -> rule5) triple3) -> rule8) OR ((((((triple1) -> rule2)) -> rule5) ((((triple2 ((((triple1) -> rule2)) -> rule5)) -> rule7) ((((triple1) -> rule2)) -> rule5)) -> rule3)) -> rule8))] Fiona is young.[(((((triple6) -> rule5) ((triple7 ((triple6) -> rule5)) -> rule3)) -> rule8))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is rough.
("Anne" "is" "rough" "+")
triple3
((((triple2 ((((triple1) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule7 % int2)) ((((triple1) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
int4
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple4
Dave is young.
("Dave" "is" "young" "+")
triple5
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple6
Fiona is white.
("Fiona" "is" "white" "+")
triple7
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple4) -> (rule5 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((triple5) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
((triple6) -> (rule5 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
((((triple4) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
((((triple6) -> (rule5 % int2))) -> (rule6 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple7 ((triple6) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
((triple2 ((((triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
((((((((triple1) -> (rule2 % int4))) -> (rule5 % int3)) triple3) -> (rule8 % int2))) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
int4
Anne is young.
("Anne" "is" "young" "+")
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2)) triple3) -> (rule8 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
((((((triple1) -> (rule2 % int5))) -> (rule5 % int4)) ((((triple2 ((((triple1) -> (rule2 % int5))) -> (rule5 % int4))) -> (rule7 % int3)) ((((triple1) -> (rule2 % int5))) -> (rule5 % int4))) -> (rule3 % int2))) -> (rule8 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
Anne is quiet.
("Anne" "is" "quiet" "+")
int5
Fiona is young.
("Fiona" "is" "young" "+")
((((triple6) -> (rule5 % int3)) ((triple7 ((triple6) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3