Bob is furry. Dave is furry. Erin is rough. Harry is young. Kind things are not green. If something is furry and green then it is rough. If something is furry then it is rough. If something is kind and young then it is rough. Rough things are kind. If something is white then it is kind.
Bob is furry.
("Bob" "is" "furry" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Harry is young.
("Harry" "is" "young" "+")
Kind things are not green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "-"))
If something is furry and green then it is rough.
((("something" "is" "furry" "+") ("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
If something is furry then it is rough.
((("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
If something is kind and young then it is rough.
((("something" "is" "kind" "+") ("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
Rough things are kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
If something is white then it is kind.
((("something" "is" "white" "+")) -> ("something" "is" "kind" "+"))
Bob is furry.
True
1
proof
[(triple1)]
("Bob" "is" "furry" "+")
triple1
Erin is not rough.
False
1
inv-proof
[(triple3)]
("Erin" "is" "rough" "-")
triple3
Dave is rough.
True
2
proof
[(((triple2) -> rule3))]
("Dave" "is" "rough" "+")
((triple2) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Bob is not rough.
False
2
inv-proof
[(((triple1) -> rule3))]
("Bob" "is" "rough" "-")
((triple1) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Erin is not green.
True
3
proof
[(((((triple3) -> rule5)) -> rule1))]
("Erin" "is" "green" "-")
((((triple3) -> (rule5 % int2))) -> (rule1 % int1))
Erin is not green.
("Erin" "is" "green" "-")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Dave is not kind.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule5))]
("Dave" "is" "kind" "-")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Bob is not green.
True
4
proof
[(((((((triple1) -> rule3)) -> rule5)) -> rule1))]
("Bob" "is" "green" "-")
((((((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Bob is not green.
("Bob" "is" "green" "-")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Dave is green.
False
4
inv-proof
[(((((((triple2) -> rule3)) -> rule5)) -> rule1))]
("Dave" "is" "green" "+")
((((((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Dave is not green.
("Dave" "is" "green" "-")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Harry is not rough.
Unknown
inv-rconc
[@3: Harry is rough.[CWA. Example of deepest failure = (rule4 <- rule5 <- rule2 <- FAIL)]]
("Harry" "is" "rough" "-")
Harry is kind.
Unknown
rconc
[@3: Harry is kind.[CWA. Example of deepest failure = (rule5 <- rule4 <- rule6 <- FAIL)]]
("Harry" "is" "kind" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Erin is young.
Unknown
random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "+")
@0: Bob is furry.[(triple1)] Dave is furry.[(triple2)] Erin is rough.[(triple3)] Harry is young.[(triple4)] @1: Bob is rough.[(((triple1) -> rule3))] Dave is rough.[(((triple2) -> rule3))] Erin is kind.[(((triple3) -> rule5))] @2: Bob is kind.[(((((triple1) -> rule3)) -> rule5))] Dave is kind.[(((((triple2) -> rule3)) -> rule5))] Erin is not green.[(((((triple3) -> rule5)) -> rule1))] @3: Bob is not green.[(((((((triple1) -> rule3)) -> rule5)) -> rule1))] Dave is not green.[(((((((triple2) -> rule3)) -> rule5)) -> rule1))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Erin is rough.
("Erin" "is" "rough" "+")
triple3
Harry is young.
("Harry" "is" "young" "+")
triple4
Bob is rough.
("Bob" "is" "rough" "+")
((triple1) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple2) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((triple3) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Erin is not green.
("Erin" "is" "green" "-")
((((triple3) -> (rule5 % int2))) -> (rule1 % int1))
Erin is not green.
("Erin" "is" "green" "-")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Bob is not green.
("Bob" "is" "green" "-")
((((((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Bob is not green.
("Bob" "is" "green" "-")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Dave is not green.
("Dave" "is" "green" "-")
((((((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Dave is not green.
("Dave" "is" "green" "-")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3