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