Bob is green. Dave is cold. Harry is furry. If something is cold then it is not furry. Cold things are kind. All green things are cold. Green things are not blue. If Harry is young then Harry is not red. All green, furry things are young. If something is red and not cold then it is young. If something is green and not furry then it is young.
Bob is green.
("Bob" "is" "green" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
If something is cold then it is not furry.
((("something" "is" "cold" "+")) -> ("something" "is" "furry" "-"))
Cold things are kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
All green things are cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
Green things are not blue.
((("something" "is" "green" "+")) -> ("something" "is" "blue" "-"))
If Harry is young then Harry is not red.
((("Harry" "is" "young" "+")) -> ("Harry" "is" "red" "-"))
All green, furry things are young.
((("something" "is" "green" "+") ("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
If something is red and not cold then it is young.
((("something" "is" "red" "+") ("something" "is" "cold" "~")) -> ("something" "is" "young" "+"))
If something is green and not furry then it is young.
((("something" "is" "green" "+") ("something" "is" "furry" "~")) -> ("something" "is" "young" "+"))
Harry is furry.
True
1
proof
[(triple3)]
("Harry" "is" "furry" "+")
triple3
Harry is not furry.
False
1
inv-proof
[(triple3)]
("Harry" "is" "furry" "-")
triple3
Bob is cold.
True
2
proof
[(((triple1) -> rule3))]
("Bob" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Dave is furry.
False
2
inv-proof
[(((triple2) -> rule1))]
("Dave" "is" "furry" "+")
((triple2) -> (rule1 % int1))
Dave is not furry.
("Dave" "is" "furry" "-")
int1
Bob is not furry.
True
3
proof
[(((((triple1) -> rule3)) -> rule1))]
("Bob" "is" "furry" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is furry.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1))]
("Bob" "is" "furry" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is young.
True
5
proof
[(((triple1 ((((triple1) -> rule3)) -> rule1)) -> rule8))]
("Bob" "is" "young" "+")
((triple1 ((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is not furry.
("Bob" "is" "furry" "-")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is not young.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule3)) -> rule1)) -> rule8))]
("Bob" "is" "young" "-")
((triple1 ((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is not furry.
("Bob" "is" "furry" "-")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Harry is not cold.
Unknown
inv-rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "cold" "-")
Harry is young.
Unknown
rconc
[@1: Harry is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "young" "+")
Harry is not kind.
Unknown
inv-rconc
[@2: Harry is kind.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Harry" "is" "kind" "-")
Dave is young.
Unknown
rconc
[@1: Dave is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "young" "+")
Bob is not red.
Unknown
inv-random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Bob is green.[(triple1)] Dave is cold.[(triple2)] Harry is furry.[(triple3)] @1: Bob is cold.[(((triple1) -> rule3))] Bob is not blue.[(((triple1) -> rule4))] Dave is kind.[(((triple2) -> rule2))] Dave is not furry.[(((triple2) -> rule1))] @2: Bob is kind.[(((((triple1) -> rule3)) -> rule2))] Bob is not furry.[(((((triple1) -> rule3)) -> rule1))] @3: Bob is young.[(((triple1 ((((triple1) -> rule3)) -> rule1)) -> rule8))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Harry is furry.
("Harry" "is" "furry" "+")
triple3
Bob is cold.
("Bob" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is not blue.
("Bob" "is" "blue" "-")
((triple1) -> (rule4 % int1))
Bob is not blue.
("Bob" "is" "blue" "-")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((triple2) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is not furry.
("Dave" "is" "furry" "-")
((triple2) -> (rule1 % int1))
Dave is not furry.
("Dave" "is" "furry" "-")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is not furry.
("Bob" "is" "furry" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
((triple1 ((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is not furry.
("Bob" "is" "furry" "-")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3