Bob is nice. Erin is nice. Gary is young. Nice things are smart. All kind things are white. Red things are white. If something is young and not smart then it is kind. All young things are kind. If Erin is furry then Erin is not white. If something is red then it is furry. If something is white then it is furry.
Bob is nice.
("Bob" "is" "nice" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Gary is young.
("Gary" "is" "young" "+")
Nice things are smart.
((("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
All kind things are white.
((("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
Red things are white.
((("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
If something is young and not smart then it is kind.
((("something" "is" "young" "+") ("something" "is" "smart" "~")) -> ("something" "is" "kind" "+"))
All young things are kind.
((("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
If Erin is furry then Erin is not white.
((("Erin" "is" "furry" "+")) -> ("Erin" "is" "white" "-"))
If something is red then it is furry.
((("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
If something is white then it is furry.
((("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
Erin is nice.
True
1
proof
[(triple2)]
("Erin" "is" "nice" "+")
triple2
Gary is not young.
False
1
inv-proof
[(triple3)]
("Gary" "is" "young" "-")
triple3
Gary is kind.
True
2
proof
[(((triple3) -> rule5))]
("Gary" "is" "kind" "+")
((triple3) -> (rule5 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Erin is not smart.
False
2
inv-proof
[(((triple2) -> rule1))]
("Erin" "is" "smart" "-")
((triple2) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Gary is white.
True
3
proof
[(((((triple3) -> rule5)) -> rule2))]
("Gary" "is" "white" "+")
((((triple3) -> (rule5 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is not white.
False
3
inv-proof
[(((((triple3) -> rule5)) -> rule2))]
("Gary" "is" "white" "-")
((((triple3) -> (rule5 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is furry.
True
4
proof
[(((((((triple3) -> rule5)) -> rule2)) -> rule8))]
("Gary" "is" "furry" "+")
((((((triple3) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is not furry.
False
4
inv-proof
[(((((((triple3) -> rule5)) -> rule2)) -> rule8))]
("Gary" "is" "furry" "-")
((((((triple3) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Bob is not kind.
Unknown
inv-rconc
[@1: Bob is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "kind" "-")
Bob is furry.
Unknown
rconc
[@3: Bob is furry.[CWA. Example of deepest failure = (rule8 <- rule2 <- rule4 <- FAIL)]]
("Bob" "is" "furry" "+")
Erin is not furry.
Unknown
inv-rconc
[@3: Erin is furry.[CWA. Example of deepest failure = (rule8 <- rule2 <- rule4 <- FAIL)]]
("Erin" "is" "furry" "-")
Gary is smart.
Unknown
rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "smart" "+")
Erin is not red.
Unknown
inv-random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Erin is young.
Unknown
random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "+")
@0: Bob is nice.[(triple1)] Erin is nice.[(triple2)] Gary is young.[(triple3)] @1: Bob is smart.[(((triple1) -> rule1))] Erin is smart.[(((triple2) -> rule1))] Gary is kind.[(((triple3) -> rule5))] @2: Gary is white.[(((((triple3) -> rule5)) -> rule2))] @3: Gary is furry.[(((((((triple3) -> rule5)) -> rule2)) -> rule8))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Erin is nice.
("Erin" "is" "nice" "+")
triple2
Gary is young.
("Gary" "is" "young" "+")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
((triple1) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple2) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((triple3) -> (rule5 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((((triple3) -> (rule5 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
((((((triple3) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3