Bob is nice. Charlie is nice. Erin is green. If someone is green then they are blue. If Bob is smart then Bob is blue. All smart people are green. If someone is white then they are rough. Kind people are nice. If Bob is green and Bob is rough then Bob is nice. All blue people are smart. If someone is nice then they are blue.
Bob is nice.
("Bob" "is" "nice" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Erin is green.
("Erin" "is" "green" "+")
If someone is green then they are blue.
((("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
If Bob is smart then Bob is blue.
((("Bob" "is" "smart" "+")) -> ("Bob" "is" "blue" "+"))
All smart people are green.
((("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
If someone is white then they are rough.
((("someone" "is" "white" "+")) -> ("someone" "is" "rough" "+"))
Kind people are nice.
((("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
If Bob is green and Bob is rough then Bob is nice.
((("Bob" "is" "green" "+") ("Bob" "is" "rough" "+")) -> ("Bob" "is" "nice" "+"))
All blue people are smart.
((("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
If someone is nice then they are blue.
((("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
Bob is nice.
True
1
proof
[(triple1)]
("Bob" "is" "nice" "+")
triple1
Erin is not green.
False
1
inv-proof
[(triple3)]
("Erin" "is" "green" "-")
triple3
Bob is blue.
True
2
proof
[(((triple1) -> rule8))]
("Bob" "is" "blue" "+")
((triple1) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Erin is not blue.
False
2
inv-proof
[(((triple3) -> rule1))]
("Erin" "is" "blue" "-")
((triple3) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is not nice.
Unknown
inv-rconc
[@1: Erin is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "nice" "-")
Bob is rough.
Unknown
rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "rough" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Bob is nice.[(triple1)] Charlie is nice.[(triple2)] Erin is green.[(triple3)] @1: Bob is blue.[(((triple1) -> rule8))] Charlie is blue.[(((triple2) -> rule8))] Erin is blue.[(((triple3) -> rule1))] @2: Bob is smart.[(((((triple1) -> rule8)) -> rule7))] Charlie is smart.[(((((triple2) -> rule8)) -> rule7))] Erin is smart.[(((((triple3) -> rule1)) -> rule7))] @3: Bob is green.[(((((((triple1) -> rule8)) -> rule7)) -> rule3))] Charlie is green.[(((((((triple2) -> rule8)) -> rule7)) -> rule3))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Erin is green.
("Erin" "is" "green" "+")
triple3
Bob is blue.
("Bob" "is" "blue" "+")
((triple1) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple2) -> (rule8 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple3) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((((triple1) -> (rule8 % int2))) -> (rule7 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple2) -> (rule8 % int2))) -> (rule7 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
((((triple3) -> (rule1 % int2))) -> (rule7 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
((((((triple1) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
((((((triple2) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3