Bob is big. Bob is smart. Erin is big. Erin is green. Erin is smart. Gary is big. Gary is furry. If someone is smart then they are kind. All kind people are round.
Bob is big.
("Bob" "is" "big" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is furry.
("Gary" "is" "furry" "+")
If someone is smart then they are kind.
((("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "+"))
All kind people are round.
((("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
Gary is furry.
True
1
proof
[(triple7)]
("Gary" "is" "furry" "+")
triple7
Bob is not smart.
False
1
inv-proof
[(triple2)]
("Bob" "is" "smart" "-")
triple2
Erin is kind.
True
2
proof
[(((triple5) -> rule1))]
("Erin" "is" "kind" "+")
((triple5) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Bob is not kind.
False
2
inv-proof
[(((triple2) -> rule1))]
("Bob" "is" "kind" "-")
((triple2) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is round.
True
3
proof
[(((((triple2) -> rule1)) -> rule2))]
("Bob" "is" "round" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is not round.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule2))]
("Bob" "is" "round" "-")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Gary is not round.
Unknown
inv-rconc
[@2: Gary is round.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Gary" "is" "round" "-")
Gary is kind.
Unknown
rconc
[@1: Gary is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "kind" "+")
Erin is not red.
Unknown
inv-random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
Bob is not green.
Unknown
inv-random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
@0: Bob is big.[(triple1)] Bob is smart.[(triple2)] Erin is big.[(triple3)] Erin is green.[(triple4)] Erin is smart.[(triple5)] Gary is big.[(triple6)] Gary is furry.[(triple7)] @1: Bob is kind.[(((triple2) -> rule1))] Erin is kind.[(((triple5) -> rule1))] @2: Bob is round.[(((((triple2) -> rule1)) -> rule2))] Erin is round.[(((((triple5) -> rule1)) -> rule2))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Erin is big.
("Erin" "is" "big" "+")
triple3
Erin is green.
("Erin" "is" "green" "+")
triple4
Erin is smart.
("Erin" "is" "smart" "+")
triple5
Gary is big.
("Gary" "is" "big" "+")
triple6
Gary is furry.
("Gary" "is" "furry" "+")
triple7
Bob is kind.
("Bob" "is" "kind" "+")
((triple2) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((triple5) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2