Bob is smart. Erin is green. All blue, green people are kind. If Bob is kind then Bob is not red. If someone is round then they are not blue. Smart, green people are not blue. Green people are nice. Nice, blue people are red. Round, red people are green. If someone is nice then they are round.
Bob is smart.
("Bob" "is" "smart" "+")
Erin is green.
("Erin" "is" "green" "+")
All blue, green people are kind.
((("someone" "is" "blue" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
If Bob is kind then Bob is not red.
((("Bob" "is" "kind" "+")) -> ("Bob" "is" "red" "-"))
If someone is round then they are not blue.
((("someone" "is" "round" "+")) -> ("someone" "is" "blue" "-"))
Smart, green people are not blue.
((("someone" "is" "smart" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "blue" "-"))
Green people are nice.
((("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
Nice, blue people are red.
((("someone" "is" "nice" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
Round, red people are green.
((("someone" "is" "round" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
If someone is nice then they are round.
((("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
Bob is smart.
True
1
proof
[(triple1)]
("Bob" "is" "smart" "+")
triple1
Bob is not smart.
False
1
inv-proof
[(triple1)]
("Bob" "is" "smart" "-")
triple1
Erin is nice.
True
2
proof
[(((triple2) -> rule5))]
("Erin" "is" "nice" "+")
((triple2) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not nice.
False
2
inv-proof
[(((triple2) -> rule5))]
("Erin" "is" "nice" "-")
((triple2) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is round.
True
3
proof
[(((((triple2) -> rule5)) -> rule8))]
("Erin" "is" "round" "+")
((((triple2) -> (rule5 % int2))) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is not round.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule8))]
("Erin" "is" "round" "-")
((((triple2) -> (rule5 % int2))) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is not blue.
True
4
proof
[(((((((triple2) -> rule5)) -> rule8)) -> rule3))]
("Erin" "is" "blue" "-")
((((((triple2) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is blue.
False
4
inv-proof
[(((((((triple2) -> rule5)) -> rule8)) -> rule3))]
("Erin" "is" "blue" "+")
((((((triple2) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Bob is not nice.
Unknown
inv-rconc
[@3: Bob is nice.[CWA. Example of deepest failure = (rule5 <- rule7 <- rule8 <- FAIL)]]
("Bob" "is" "nice" "-")
Bob is round.
Unknown
rconc
[@3: Bob is round.[CWA. Example of deepest failure = (rule8 <- rule5 <- rule7 <- FAIL)]]
("Bob" "is" "round" "+")
Erin is not red.
Unknown
inv-rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "red" "-")
Bob is red.
Unknown
rconc
[@1: Bob is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "red" "+")
Erin is not smart.
Unknown
inv-random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
@0: Bob is smart.[(triple1)] Erin is green.[(triple2)] @1: Erin is nice.[(((triple2) -> rule5))] @2: Erin is round.[(((((triple2) -> rule5)) -> rule8))] @3: Erin is not blue.[(((((((triple2) -> rule5)) -> rule8)) -> rule3))]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Erin is green.
("Erin" "is" "green" "+")
triple2
Erin is nice.
("Erin" "is" "nice" "+")
((triple2) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
((((triple2) -> (rule5 % int2))) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is not blue.
("Erin" "is" "blue" "-")
((((((triple2) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3