Bob is young. Gary is rough. If someone is rough then they are smart. All young, smart people are kind. If Gary is rough then Gary is big. Kind, furry people are rough. If Bob is smart and Bob is kind then Bob is rough. If someone is young then they are smart.
Bob is young.
("Bob" "is" "young" "+")
Gary is rough.
("Gary" "is" "rough" "+")
If someone is rough then they are smart.
((("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
All young, smart people are kind.
((("someone" "is" "young" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "+"))
If Gary is rough then Gary is big.
((("Gary" "is" "rough" "+")) -> ("Gary" "is" "big" "+"))
Kind, furry people are rough.
((("someone" "is" "kind" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
If Bob is smart and Bob is kind then Bob is rough.
((("Bob" "is" "smart" "+") ("Bob" "is" "kind" "+")) -> ("Bob" "is" "rough" "+"))
If someone is young then they are smart.
((("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
Gary is rough.
True
1
proof
[(triple2)]
("Gary" "is" "rough" "+")
triple2
Bob is not young.
False
1
inv-proof
[(triple1)]
("Bob" "is" "young" "-")
triple1
Bob is smart.
True
2
proof
[(((triple1) -> rule6))]
("Bob" "is" "smart" "+")
((triple1) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Gary is not big.
False
2
inv-proof
[(((triple2) -> rule3))]
("Gary" "is" "big" "-")
((triple2) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Bob is kind.
True
4
proof
[(((triple1 ((triple1) -> rule6)) -> rule2))]
("Bob" "is" "kind" "+")
((triple1 ((triple1) -> (rule6 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is not kind.
False
4
inv-proof
[(((triple1 ((triple1) -> rule6)) -> rule2))]
("Bob" "is" "kind" "-")
((triple1 ((triple1) -> (rule6 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is rough.
True
7
proof
[(((((triple1) -> rule6) ((triple1 ((triple1) -> rule6)) -> rule2)) -> rule5))]
("Bob" "is" "rough" "+")
((((triple1) -> (rule6 % int3)) ((triple1 ((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is not rough.
False
7
inv-proof
[(((((triple1) -> rule6) ((triple1 ((triple1) -> rule6)) -> rule2)) -> rule5))]
("Bob" "is" "rough" "-")
((((triple1) -> (rule6 % int3)) ((triple1 ((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Gary is not kind.
Unknown
inv-rconc
[@1: Gary is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "kind" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
Gary is not young.
Unknown
inv-random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
Gary is not white.
Unknown
inv-random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
@0: Bob is young.[(triple1)] Gary is rough.[(triple2)] @1: Bob is smart.[(((triple1) -> rule6))] Gary is big.[(((triple2) -> rule3))] Gary is smart.[(((triple2) -> rule1))] @2: Bob is kind.[(((triple1 ((triple1) -> rule6)) -> rule2))] @3: Bob is rough.[(((((triple1) -> rule6) ((triple1 ((triple1) -> rule6)) -> rule2)) -> rule5))]
Bob is young.
("Bob" "is" "young" "+")
triple1
Gary is rough.
("Gary" "is" "rough" "+")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
((triple1) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple2) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple2) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((triple1 ((triple1) -> (rule6 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
((((triple1) -> (rule6 % int3)) ((triple1 ((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3