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