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