Bob is blue. Bob is rough. Bob is young. Dave is cold. Dave is furry. Dave is kind. Erin is kind. Erin is rough. Erin is young. Harry is blue. Harry is cold. Harry is furry. Harry is kind. Harry is smart. Harry is young. All rough things are smart. Smart, kind things are cold. Furry things are rough. All rough things are blue. All cold, blue things are furry. If Harry is kind then Harry is cold. All young things are smart. If Bob is cold and Bob is furry then Bob is smart.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
All rough things are smart.
((("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
Smart, kind things are cold.
((("something" "is" "smart" "+") ("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
Furry things are rough.
((("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
All rough things are blue.
((("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
All cold, blue things are furry.
((("something" "is" "cold" "+") ("something" "is" "blue" "+")) -> ("something" "is" "furry" "+"))
If Harry is kind then Harry is cold.
((("Harry" "is" "kind" "+")) -> ("Harry" "is" "cold" "+"))
All young things are smart.
((("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
If Bob is cold and Bob is furry then Bob is smart.
((("Bob" "is" "cold" "+") ("Bob" "is" "furry" "+")) -> ("Bob" "is" "smart" "+"))
Dave is cold.
True
1
proof
[(triple4 OR ((((((triple5) -> rule3)) -> rule1) triple6) -> rule2))]
("Dave" "is" "cold" "+")
triple4
((((((triple5) -> (rule3 % int3))) -> (rule1 % int2)) triple6) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Harry is not furry.
False
1
inv-proof
[(triple12 OR ((triple11 triple10) -> rule5) OR ((((triple13) -> rule6) triple10) -> rule5) OR ((((triple14 triple13) -> rule2) triple10) -> rule5) OR ((((((triple15) -> rule7) triple13) -> rule2) triple10) -> rule5))]
("Harry" "is" "furry" "-")
triple12
((triple11 triple10) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((((triple13) -> (rule6 % int2)) triple10) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((triple14 triple13) -> (rule2 % int2)) triple10) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((((triple15) -> (rule7 % int3)) triple13) -> (rule2 % int2)) triple10) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Bob is smart.
True
2
proof
[(((triple2) -> rule1) OR ((triple3) -> rule7))]
("Bob" "is" "smart" "+")
((triple2) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple3) -> (rule7 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is not smart.
False
2
inv-proof
[(((triple2) -> rule1) OR ((triple3) -> rule7))]
("Bob" "is" "smart" "-")
((triple2) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple3) -> (rule7 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Dave is smart.
True
3
proof
[(((((triple5) -> rule3)) -> rule1))]
("Dave" "is" "smart" "+")
((((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is not blue.
False
3
inv-proof
[(((((triple5) -> rule3)) -> rule4))]
("Dave" "is" "blue" "-")
((((triple5) -> (rule3 % int2))) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Erin is furry.
True
7
proof
[(((((((triple8) -> rule1) triple7) -> rule2) ((triple8) -> rule4)) -> rule5) OR ((((((triple9) -> rule7) triple7) -> rule2) ((triple8) -> rule4)) -> rule5))]
("Erin" "is" "furry" "+")
((((((triple8) -> (rule1 % int4)) triple7) -> (rule2 % int3)) ((triple8) -> (rule4 % int2))) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
((((((triple9) -> (rule7 % int4)) triple7) -> (rule2 % int3)) ((triple8) -> (rule4 % int2))) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Erin is not furry.
False
7
inv-proof
[(((((((triple8) -> rule1) triple7) -> rule2) ((triple8) -> rule4)) -> rule5) OR ((((((triple9) -> rule7) triple7) -> rule2) ((triple8) -> rule4)) -> rule5))]
("Erin" "is" "furry" "-")
((((((triple8) -> (rule1 % int4)) triple7) -> (rule2 % int3)) ((triple8) -> (rule4 % int2))) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
((((((triple9) -> (rule7 % int4)) triple7) -> (rule2 % int3)) ((triple8) -> (rule4 % int2))) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Bob is not furry.
Unknown
inv-rconc
[@2: Bob is furry.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("Bob" "is" "furry" "-")
Bob is cold.
Unknown
rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "cold" "+")
Dave is not young.
Unknown
inv-random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Bob is blue.[(triple1 OR ((triple2) -> rule4))] Bob is rough.[(triple2)] Bob is young.[(triple3)] Dave is cold.[(triple4 OR ((((((triple5) -> rule3)) -> rule1) triple6) -> rule2))] Dave is furry.[(triple5)] Dave is kind.[(triple6)] Erin is kind.[(triple7)] Erin is rough.[(triple8)] Erin is young.[(triple9)] Harry is blue.[(triple10 OR ((((triple12) -> rule3)) -> rule4))] Harry is cold.[(triple11 OR ((triple13) -> rule6) OR ((triple14 triple13) -> rule2) OR ((((triple15) -> rule7) triple13) -> rule2) OR ((((((triple12) -> rule3)) -> rule1) triple13) -> rule2))] Harry is furry.[(triple12 OR ((triple11 triple10) -> rule5) OR ((((triple13) -> rule6) triple10) -> rule5) OR ((((triple14 triple13) -> rule2) triple10) -> rule5) OR ((((((triple15) -> rule7) triple13) -> rule2) triple10) -> rule5))] Harry is kind.[(triple13)] Harry is smart.[(triple14 OR ((triple15) -> rule7) OR ((((triple12) -> rule3)) -> rule1) OR ((((((triple11 triple10) -> rule5)) -> rule3)) -> rule1) OR ((((((((triple13) -> rule6) triple10) -> rule5)) -> rule3)) -> rule1))] Harry is young.[(triple15)] @1: Bob is smart.[(((triple2) -> rule1) OR ((triple3) -> rule7))] Dave is rough.[(((triple5) -> rule3))] Erin is blue.[(((triple8) -> rule4))] Erin is smart.[(((triple8) -> rule1) OR ((triple9) -> rule7))] Harry is rough.[(((triple12) -> rule3) OR ((((triple11 triple10) -> rule5)) -> rule3) OR ((((((triple13) -> rule6) triple10) -> rule5)) -> rule3) OR ((((((triple14 triple13) -> rule2) triple10) -> rule5)) -> rule3) OR ((((((((triple15) -> rule7) triple13) -> rule2) triple10) -> rule5)) -> rule3))] @2: Dave is blue.[(((((triple5) -> rule3)) -> rule4))] Dave is smart.[(((((triple5) -> rule3)) -> rule1))] Erin is cold.[(((((triple8) -> rule1) triple7) -> rule2) OR ((((triple9) -> rule7) triple7) -> rule2))] @3: Erin is furry.[(((((((triple8) -> rule1) triple7) -> rule2) ((triple8) -> rule4)) -> rule5) OR ((((((triple9) -> rule7) triple7) -> rule2) ((triple8) -> rule4)) -> rule5))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
((triple2) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Bob is young.
("Bob" "is" "young" "+")
triple3
Dave is cold.
("Dave" "is" "cold" "+")
triple4
((((((triple5) -> (rule3 % int3))) -> (rule1 % int2)) triple6) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
triple5
Dave is kind.
("Dave" "is" "kind" "+")
triple6
Erin is kind.
("Erin" "is" "kind" "+")
triple7
Erin is rough.
("Erin" "is" "rough" "+")
triple8
Erin is young.
("Erin" "is" "young" "+")
triple9
Harry is blue.
("Harry" "is" "blue" "+")
triple10
((((triple12) -> (rule3 % int2))) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
triple11
((triple13) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((triple14 triple13) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((((triple15) -> (rule7 % int2)) triple13) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((((((triple12) -> (rule3 % int3))) -> (rule1 % int2)) triple13) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
triple12
((triple11 triple10) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((((triple13) -> (rule6 % int2)) triple10) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((triple14 triple13) -> (rule2 % int2)) triple10) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((((triple15) -> (rule7 % int3)) triple13) -> (rule2 % int2)) triple10) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
triple13
Harry is smart.
("Harry" "is" "smart" "+")
triple14
((triple15) -> (rule7 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((((triple12) -> (rule3 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((((triple11 triple10) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
((((((((triple13) -> (rule6 % int4)) triple10) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
Harry is young.
("Harry" "is" "young" "+")
triple15
Bob is smart.
("Bob" "is" "smart" "+")
((triple2) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple3) -> (rule7 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple5) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple8) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple8) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((triple9) -> (rule7 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple12) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple11 triple10) -> (rule5 % int2))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((((triple13) -> (rule6 % int3)) triple10) -> (rule5 % int2))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
((((((triple14 triple13) -> (rule2 % int3)) triple10) -> (rule5 % int2))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
((((((((triple15) -> (rule7 % int4)) triple13) -> (rule2 % int3)) triple10) -> (rule5 % int2))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
Dave is blue.
("Dave" "is" "blue" "+")
((((triple5) -> (rule3 % int2))) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
((((triple8) -> (rule1 % int2)) triple7) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((triple9) -> (rule7 % int2)) triple7) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
((((((triple8) -> (rule1 % int4)) triple7) -> (rule2 % int3)) ((triple8) -> (rule4 % int2))) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
((((((triple9) -> (rule7 % int4)) triple7) -> (rule2 % int3)) ((triple8) -> (rule4 % int2))) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4