Bob is cold. Bob is furry. Bob is rough. Charlie is cold. Charlie is smart. Dave is cold. Dave is quiet. Dave is rough. Dave is round. Dave is white. Harry is quiet. Harry is round. If someone is cold and round then they are smart. Quiet, furry people are smart. If someone is round and smart then they are white. All quiet, round people are rough. All rough people are furry. Furry, round people are cold.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is round.
("Harry" "is" "round" "+")
If someone is cold and round then they are smart.
((("someone" "is" "cold" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
Quiet, furry people are smart.
((("someone" "is" "quiet" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "+"))
If someone is round and smart then they are white.
((("someone" "is" "round" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "white" "+"))
All quiet, round people are rough.
((("someone" "is" "quiet" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
All rough people are furry.
((("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "+"))
Furry, round people are cold.
((("someone" "is" "furry" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
Dave is rough.
True
1
proof
[(triple8 OR ((triple7 triple9) -> rule4))]
("Dave" "is" "rough" "+")
triple8
((triple7 triple9) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Bob is not rough.
False
1
inv-proof
[(triple3)]
("Bob" "is" "rough" "-")
triple3
Harry is rough.
True
3
proof
[(((triple11 triple12) -> rule4))]
("Harry" "is" "rough" "+")
((triple11 triple12) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Dave is not smart.
False
3
inv-proof
[(((triple6 triple9) -> rule1) OR ((triple7 ((triple8) -> rule5)) -> rule2) OR ((triple7 ((((triple7 triple9) -> rule4)) -> rule5)) -> rule2) OR ((((((triple8) -> rule5) triple9) -> rule6) triple9) -> rule1) OR ((((((((triple7 triple9) -> rule4)) -> rule5) triple9) -> rule6) triple9) -> rule1))]
("Dave" "is" "smart" "-")
((triple6 triple9) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((triple7 ((triple8) -> (rule5 % int2))) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
((triple7 ((((triple7 triple9) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((((((triple8) -> (rule5 % int3)) triple9) -> (rule6 % int2)) triple9) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
((((((((triple7 triple9) -> (rule4 % int4))) -> (rule5 % int3)) triple9) -> (rule6 % int2)) triple9) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Harry is furry.
True
4
proof
[(((((triple11 triple12) -> rule4)) -> rule5))]
("Harry" "is" "furry" "+")
((((triple11 triple12) -> (rule4 % int2))) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is not furry.
False
4
inv-proof
[(((((triple11 triple12) -> rule4)) -> rule5))]
("Harry" "is" "furry" "-")
((((triple11 triple12) -> (rule4 % int2))) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is cold.
True
6
proof
[(((((((triple11 triple12) -> rule4)) -> rule5) triple12) -> rule6))]
("Harry" "is" "cold" "+")
((((((triple11 triple12) -> (rule4 % int3))) -> (rule5 % int2)) triple12) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is not cold.
False
6
inv-proof
[(((((((triple11 triple12) -> rule4)) -> rule5) triple12) -> rule6))]
("Harry" "is" "cold" "-")
((((((triple11 triple12) -> (rule4 % int3))) -> (rule5 % int2)) triple12) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Bob is not white.
Unknown
inv-rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "white" "-")
Charlie is furry.
Unknown
rconc
[@2: Charlie is furry.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("Charlie" "is" "furry" "+")
Bob is not smart.
Unknown
inv-rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "smart" "-")
Charlie is white.
Unknown
rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "white" "+")
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
@0: Bob is cold.[(triple1)] Bob is furry.[(triple2 OR ((triple3) -> rule5))] Bob is rough.[(triple3)] Charlie is cold.[(triple4)] Charlie is smart.[(triple5)] Dave is cold.[(triple6 OR ((((triple8) -> rule5) triple9) -> rule6) OR ((((((triple7 triple9) -> rule4)) -> rule5) triple9) -> rule6))] Dave is quiet.[(triple7)] Dave is rough.[(triple8 OR ((triple7 triple9) -> rule4))] Dave is round.[(triple9)] Dave is white.[(triple10 OR ((triple9 ((triple6 triple9) -> rule1)) -> rule3) OR ((triple9 ((triple7 ((triple8) -> rule5)) -> rule2)) -> rule3) OR ((triple9 ((triple7 ((((triple7 triple9) -> rule4)) -> rule5)) -> rule2)) -> rule3) OR ((triple9 ((((((triple8) -> rule5) triple9) -> rule6) triple9) -> rule1)) -> rule3) OR ((triple9 ((((((((triple7 triple9) -> rule4)) -> rule5) triple9) -> rule6) triple9) -> rule1)) -> rule3))] Harry is quiet.[(triple11)] Harry is round.[(triple12)] @1: Dave is furry.[(((triple8) -> rule5) OR ((((triple7 triple9) -> rule4)) -> rule5))] Dave is smart.[(((triple6 triple9) -> rule1) OR ((triple7 ((triple8) -> rule5)) -> rule2) OR ((triple7 ((((triple7 triple9) -> rule4)) -> rule5)) -> rule2) OR ((((((triple8) -> rule5) triple9) -> rule6) triple9) -> rule1) OR ((((((((triple7 triple9) -> rule4)) -> rule5) triple9) -> rule6) triple9) -> rule1))] Harry is rough.[(((triple11 triple12) -> rule4))] @2: Harry is furry.[(((((triple11 triple12) -> rule4)) -> rule5))] @3: Harry is cold.[(((((((triple11 triple12) -> rule4)) -> rule5) triple12) -> rule6))] Harry is smart.[(((triple11 ((((triple11 triple12) -> rule4)) -> rule5)) -> rule2) OR ((((((((triple11 triple12) -> rule4)) -> rule5) triple12) -> rule6) triple12) -> rule1))] @4: Harry is white.[(((triple12 ((triple11 ((((triple11 triple12) -> rule4)) -> rule5)) -> rule2)) -> rule3) OR ((triple12 ((((((((triple11 triple12) -> rule4)) -> rule5) triple12) -> rule6) triple12) -> rule1)) -> rule3))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
((triple3) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
triple3
Charlie is cold.
("Charlie" "is" "cold" "+")
triple4
Charlie is smart.
("Charlie" "is" "smart" "+")
triple5
Dave is cold.
("Dave" "is" "cold" "+")
triple6
((((triple8) -> (rule5 % int2)) triple9) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
((((((triple7 triple9) -> (rule4 % int3))) -> (rule5 % int2)) triple9) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
triple7
Dave is rough.
("Dave" "is" "rough" "+")
triple8
((triple7 triple9) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple9
Dave is white.
("Dave" "is" "white" "+")
triple10
((triple9 ((triple6 triple9) -> (rule1 % int2))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((triple9 ((triple7 ((triple8) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
((triple9 ((triple7 ((((triple7 triple9) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
((triple9 ((((((triple8) -> (rule5 % int4)) triple9) -> (rule6 % int3)) triple9) -> (rule1 % int2))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
int4
((triple9 ((((((((triple7 triple9) -> (rule4 % int5))) -> (rule5 % int4)) triple9) -> (rule6 % int3)) triple9) -> (rule1 % int2))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
int4
Dave is rough.
("Dave" "is" "rough" "+")
int5
Harry is quiet.
("Harry" "is" "quiet" "+")
triple11
Harry is round.
("Harry" "is" "round" "+")
triple12
Dave is furry.
("Dave" "is" "furry" "+")
((triple8) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((((triple7 triple9) -> (rule4 % int2))) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((triple6 triple9) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((triple7 ((triple8) -> (rule5 % int2))) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
((triple7 ((((triple7 triple9) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((((((triple8) -> (rule5 % int3)) triple9) -> (rule6 % int2)) triple9) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
((((((((triple7 triple9) -> (rule4 % int4))) -> (rule5 % int3)) triple9) -> (rule6 % int2)) triple9) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Harry is rough.
("Harry" "is" "rough" "+")
((triple11 triple12) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((((triple11 triple12) -> (rule4 % int2))) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
((((((triple11 triple12) -> (rule4 % int3))) -> (rule5 % int2)) triple12) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
((triple11 ((((triple11 triple12) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
((((((((triple11 triple12) -> (rule4 % int4))) -> (rule5 % int3)) triple12) -> (rule6 % int2)) triple12) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is white.
("Harry" "is" "white" "+")
((triple12 ((triple11 ((((triple11 triple12) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
((triple12 ((((((((triple11 triple12) -> (rule4 % int5))) -> (rule5 % int4)) triple12) -> (rule6 % int3)) triple12) -> (rule1 % int2))) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4
Harry is rough.
("Harry" "is" "rough" "+")
int5