Bob is young. Dave is rough. Erin is green. If something is red and kind then it is young. All nice, rough things are furry. All red things are kind. All red, kind things are furry. Kind things are young. If something is nice then it is young. All young things are red. All red things are furry.
Bob is young.
("Bob" "is" "young" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Erin is green.
("Erin" "is" "green" "+")
If something is red and kind then it is young.
((("something" "is" "red" "+") ("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
All nice, rough things are furry.
((("something" "is" "nice" "+") ("something" "is" "rough" "+")) -> ("something" "is" "furry" "+"))
All red things are kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
All red, kind things are furry.
((("something" "is" "red" "+") ("something" "is" "kind" "+")) -> ("something" "is" "furry" "+"))
Kind things are young.
((("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
If something is nice then it is young.
((("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
All young things are red.
((("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
All red things are furry.
((("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
Bob is young.
True
1
proof
[(triple1)]
("Bob" "is" "young" "+")
triple1
Erin is not green.
False
1
inv-proof
[(triple3)]
("Erin" "is" "green" "-")
triple3
Bob is red.
True
2
proof
[(((triple1) -> rule7))]
("Bob" "is" "red" "+")
((triple1) -> (rule7 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is not red.
False
2
inv-proof
[(((triple1) -> rule7))]
("Bob" "is" "red" "-")
((triple1) -> (rule7 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Dave is not young.
Unknown
inv-rconc
[@4: Dave is young.[CWA. Example of deepest failure = (rule1 <- rule7 <- rule5 <- rule3 <- FAIL)]]
("Dave" "is" "young" "-")
Dave is furry.
Unknown
rconc
[@4: Dave is furry.[CWA. Example of deepest failure = (rule4 <- rule7 <- rule5 <- rule3 <- FAIL)]]
("Dave" "is" "furry" "+")
Dave is not nice.
Unknown
inv-random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "-")
Erin is nice.
Unknown
random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "+")
@0: Bob is young.[(triple1)] Dave is rough.[(triple2)] Erin is green.[(triple3)] @1: Bob is red.[(((triple1) -> rule7))] @2: Bob is furry.[(((((triple1) -> rule7)) -> rule8) OR ((((triple1) -> rule7) ((((triple1) -> rule7)) -> rule3)) -> rule4))] Bob is kind.[(((((triple1) -> rule7)) -> rule3))]
Bob is young.
("Bob" "is" "young" "+")
triple1
Dave is rough.
("Dave" "is" "rough" "+")
triple2
Erin is green.
("Erin" "is" "green" "+")
triple3
Bob is red.
("Bob" "is" "red" "+")
((triple1) -> (rule7 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((((triple1) -> (rule7 % int2))) -> (rule8 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((((triple1) -> (rule7 % int3)) ((((triple1) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
((((triple1) -> (rule7 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2