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