Bob is cold. Bob is furry. Bob is not smart. Dave is kind. Dave is smart. Harry is blue. Harry is furry. Harry is kind. Harry is nice. Harry is smart. If something is smart then it is cold. Green things are cold. All smart things are furry. If Dave is kind then Dave is green. Blue things are nice. If something is green then it is nice.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is not smart.
("Bob" "is" "smart" "-")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If something is smart then it is cold.
((("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
Green things are cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
All smart things are furry.
((("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
If Dave is kind then Dave is green.
((("Dave" "is" "kind" "+")) -> ("Dave" "is" "green" "+"))
Blue things are nice.
((("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
If something is green then it is nice.
((("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
Harry is nice.
True
1
proof
[(triple9 OR ((triple6) -> rule5))]
("Harry" "is" "nice" "+")
triple9
((triple6) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is not smart.
False
1
inv-proof
[(triple10)]
("Harry" "is" "smart" "-")
triple10
Harry is cold.
True
2
proof
[(((triple10) -> rule1))]
("Harry" "is" "cold" "+")
((triple10) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Dave is not cold.
False
2
inv-proof
[(((triple5) -> rule1) OR ((((triple4) -> rule4)) -> rule2))]
("Dave" "is" "cold" "-")
((triple5) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((((triple4) -> (rule4 % int2))) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is nice.
True
3
proof
[(((((triple4) -> rule4)) -> rule6))]
("Dave" "is" "nice" "+")
((((triple4) -> (rule4 % int2))) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is not nice.
False
3
inv-proof
[(((((triple4) -> rule4)) -> rule6))]
("Dave" "is" "nice" "-")
((((triple4) -> (rule4 % int2))) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Bob is not nice.
Unknown
inv-rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "nice" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
Bob is not green.
Unknown
inv-random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Bob is cold.[(triple1)] Bob is furry.[(triple2)] Bob is not smart.[(triple3)] Dave is kind.[(triple4)] Dave is smart.[(triple5)] Harry is blue.[(triple6)] Harry is furry.[(triple7 OR ((triple10) -> rule3))] Harry is kind.[(triple8)] Harry is nice.[(triple9 OR ((triple6) -> rule5))] Harry is smart.[(triple10)] @1: Dave is cold.[(((triple5) -> rule1) OR ((((triple4) -> rule4)) -> rule2))] Dave is furry.[(((triple5) -> rule3))] Dave is green.[(((triple4) -> rule4))] Harry is cold.[(((triple10) -> rule1))] @2: Dave is nice.[(((((triple4) -> rule4)) -> rule6))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is not smart.
("Bob" "is" "smart" "-")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
triple4
Dave is smart.
("Dave" "is" "smart" "+")
triple5
Harry is blue.
("Harry" "is" "blue" "+")
triple6
Harry is furry.
("Harry" "is" "furry" "+")
triple7
((triple10) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
triple8
Harry is nice.
("Harry" "is" "nice" "+")
triple9
((triple6) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
triple10
Dave is cold.
("Dave" "is" "cold" "+")
((triple5) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((((triple4) -> (rule4 % int2))) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
((triple5) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((triple4) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple10) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((((triple4) -> (rule4 % int2))) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2