Bob is smart. Erin is white. Gary is nice. Kind things are smart. Big things are nice. All rough things are nice. All green, kind things are smart. If something is nice then it is green. All rough, big things are white. If something is rough then it is nice. If something is green then it is white.
Bob is smart.
("Bob" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Kind things are smart.
((("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
Big things are nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
All rough things are nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
All green, kind things are smart.
((("something" "is" "green" "+") ("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
If something is nice then it is green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
All rough, big things are white.
((("something" "is" "rough" "+") ("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
If something is rough then it is nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
If something is green then it is white.
((("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
Gary is nice.
True
1
proof
[(triple3)]
("Gary" "is" "nice" "+")
triple3
Erin is not white.
False
1
inv-proof
[(triple2)]
("Erin" "is" "white" "-")
triple2
Gary is green.
True
2
proof
[(((triple3) -> rule5))]
("Gary" "is" "green" "+")
((triple3) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is not green.
False
2
inv-proof
[(((triple3) -> rule5))]
("Gary" "is" "green" "-")
((triple3) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is white.
True
3
proof
[(((((triple3) -> rule5)) -> rule8))]
("Gary" "is" "white" "+")
((((triple3) -> (rule5 % int2))) -> (rule8 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is not white.
False
3
inv-proof
[(((((triple3) -> rule5)) -> rule8))]
("Gary" "is" "white" "-")
((((triple3) -> (rule5 % int2))) -> (rule8 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Erin is not nice.
Unknown
inv-rconc
[@1: Erin is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "nice" "-")
Erin is smart.
Unknown
rconc
[@1: Erin is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "smart" "+")
Bob is not white.
Unknown
inv-rconc
[@3: Bob is white.[CWA. Example of deepest failure = (rule8 <- rule5 <- rule2 <- FAIL)]]
("Bob" "is" "white" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Gary is rough.
Unknown
random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "+")
@0: Bob is smart.[(triple1)] Erin is white.[(triple2)] Gary is nice.[(triple3)] @1: Gary is green.[(((triple3) -> rule5))] @2: Gary is white.[(((((triple3) -> rule5)) -> rule8))]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Erin is white.
("Erin" "is" "white" "+")
triple2
Gary is nice.
("Gary" "is" "nice" "+")
triple3
Gary is green.
("Gary" "is" "green" "+")
((triple3) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((((triple3) -> (rule5 % int2))) -> (rule8 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2