Anne is not blue. Anne is furry. Anne is green. Anne is quiet. Anne is rough. Bob is furry. Dave is rough. Erin is quiet. Erin is round. Erin is not young. All round things are quiet. If Bob is rough and Bob is quiet then Bob is blue. Green, blue things are young. If something is rough then it is young. If something is blue then it is not furry. If something is young then it is furry. Furry things are green. If Bob is blue and Bob is young then Bob is quiet. All green things are round.
Anne is not blue.
("Anne" "is" "blue" "-")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is not young.
("Erin" "is" "young" "-")
All round things are quiet.
((("something" "is" "round" "+")) -> ("something" "is" "quiet" "+"))
If Bob is rough and Bob is quiet then Bob is blue.
((("Bob" "is" "rough" "+") ("Bob" "is" "quiet" "+")) -> ("Bob" "is" "blue" "+"))
Green, blue things are young.
((("something" "is" "green" "+") ("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
If something is rough then it is young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
If something is blue then it is not furry.
((("something" "is" "blue" "+")) -> ("something" "is" "furry" "-"))
If something is young then it is furry.
((("something" "is" "young" "+")) -> ("something" "is" "furry" "+"))
Furry things are green.
((("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
If Bob is blue and Bob is young then Bob is quiet.
((("Bob" "is" "blue" "+") ("Bob" "is" "young" "+")) -> ("Bob" "is" "quiet" "+"))
All green things are round.
((("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
Dave is rough.
True
1
proof
[(triple7)]
("Dave" "is" "rough" "+")
triple7
Bob is not furry.
False
1
inv-proof
[(triple6)]
("Bob" "is" "furry" "-")
triple6
Bob is green.
True
2
proof
[(((triple6) -> rule7))]
("Bob" "is" "green" "+")
((triple6) -> (rule7 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Anne is not young.
False
2
inv-proof
[(((triple5) -> rule4))]
("Anne" "is" "young" "-")
((triple5) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Bob is round.
True
3
proof
[(((((triple6) -> rule7)) -> rule9))]
("Bob" "is" "round" "+")
((((triple6) -> (rule7 % int2))) -> (rule9 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is not round.
False
3
inv-proof
[(((((triple6) -> rule7)) -> rule9))]
("Bob" "is" "round" "-")
((((triple6) -> (rule7 % int2))) -> (rule9 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is quiet.
True
4
proof
[(((((((triple6) -> rule7)) -> rule9)) -> rule1))]
("Bob" "is" "quiet" "+")
((((((triple6) -> (rule7 % int3))) -> (rule9 % int2))) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is not quiet.
False
4
inv-proof
[(((((((triple6) -> rule7)) -> rule9)) -> rule1))]
("Bob" "is" "quiet" "-")
((((((triple6) -> (rule7 % int3))) -> (rule9 % int2))) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Dave is round.
True
5
proof
[(((((((((triple7) -> rule4)) -> rule6)) -> rule7)) -> rule9))]
("Dave" "is" "round" "+")
((((((((triple7) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule9 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
Dave is not round.
False
5
inv-proof
[(((((((((triple7) -> rule4)) -> rule6)) -> rule7)) -> rule9))]
("Dave" "is" "round" "-")
((((((((triple7) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule9 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
Dave is quiet.
True
6
proof
[(((((((((((triple7) -> rule4)) -> rule6)) -> rule7)) -> rule9)) -> rule1))]
("Dave" "is" "quiet" "+")
((((((((((triple7) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule9 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
int4
Dave is young.
("Dave" "is" "young" "+")
int5
Dave is not quiet.
False
6
inv-proof
[(((((((((((triple7) -> rule4)) -> rule6)) -> rule7)) -> rule9)) -> rule1))]
("Dave" "is" "quiet" "-")
((((((((((triple7) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule9 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
int4
Dave is young.
("Dave" "is" "young" "+")
int5
Erin is not furry.
Unknown
inv-rconc
[@1: Erin is furry.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "furry" "-")
Erin is green.
Unknown
rconc
[@2: Erin is green.[CWA. Example of deepest failure = (rule7 <- rule6 <- FAIL)]]
("Erin" "is" "green" "+")
Bob is not blue.
Unknown
inv-rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "blue" "-")
Bob is young.
Unknown
rconc
[@2: Bob is young.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Bob" "is" "young" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
Erin is not rough.
Unknown
inv-random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
@0: Anne is furry.[(triple2 OR ((((triple5) -> rule4)) -> rule6))] Anne is green.[(triple3 OR ((triple2) -> rule7) OR ((((((triple5) -> rule4)) -> rule6)) -> rule7))] Anne is not blue.[(triple1)] Anne is quiet.[(triple4 OR ((((triple3) -> rule9)) -> rule1) OR ((((((triple2) -> rule7)) -> rule9)) -> rule1) OR ((((((((((triple5) -> rule4)) -> rule6)) -> rule7)) -> rule9)) -> rule1))] Anne is rough.[(triple5)] Bob is furry.[(triple6)] Dave is rough.[(triple7)] Erin is not young.[(triple10)] Erin is quiet.[(triple8 OR ((triple9) -> rule1))] Erin is round.[(triple9)] @1: Anne is round.[(((triple3) -> rule9) OR ((((triple2) -> rule7)) -> rule9) OR ((((((((triple5) -> rule4)) -> rule6)) -> rule7)) -> rule9))] Anne is young.[(((triple5) -> rule4))] Bob is green.[(((triple6) -> rule7))] Dave is young.[(((triple7) -> rule4))] @2: Bob is round.[(((((triple6) -> rule7)) -> rule9))] Dave is furry.[(((((triple7) -> rule4)) -> rule6))] @3: Bob is quiet.[(((((((triple6) -> rule7)) -> rule9)) -> rule1))] Dave is green.[(((((((triple7) -> rule4)) -> rule6)) -> rule7))] @4: Dave is round.[(((((((((triple7) -> rule4)) -> rule6)) -> rule7)) -> rule9))] @5: Dave is quiet.[(((((((((((triple7) -> rule4)) -> rule6)) -> rule7)) -> rule9)) -> rule1))]
Anne is furry.
("Anne" "is" "furry" "+")
triple2
((((triple5) -> (rule4 % int2))) -> (rule6 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
triple3
((triple2) -> (rule7 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((((((triple5) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is not blue.
("Anne" "is" "blue" "-")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple4
((((triple3) -> (rule9 % int2))) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
((((((triple2) -> (rule7 % int3))) -> (rule9 % int2))) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
((((((((((triple5) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule9 % int2))) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
Anne is young.
("Anne" "is" "young" "+")
int5
Anne is rough.
("Anne" "is" "rough" "+")
triple5
Bob is furry.
("Bob" "is" "furry" "+")
triple6
Dave is rough.
("Dave" "is" "rough" "+")
triple7
Erin is not young.
("Erin" "is" "young" "-")
triple10
Erin is quiet.
("Erin" "is" "quiet" "+")
triple8
((triple9) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
triple9
Anne is round.
("Anne" "is" "round" "+")
((triple3) -> (rule9 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((((triple2) -> (rule7 % int2))) -> (rule9 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((((((((triple5) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule9 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is young.
("Anne" "is" "young" "+")
((triple5) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((triple6) -> (rule7 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple7) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((((triple6) -> (rule7 % int2))) -> (rule9 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
((((triple7) -> (rule4 % int2))) -> (rule6 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
((((((triple6) -> (rule7 % int3))) -> (rule9 % int2))) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
((((((triple7) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
((((((((triple7) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule9 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
Dave is quiet.
("Dave" "is" "quiet" "+")
((((((((((triple7) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule9 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
int4
Dave is young.
("Dave" "is" "young" "+")
int5