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