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