Bob is blue. Bob is rough. Erin is blue. Erin is smart. Fiona is blue. Gary is nice. Gary is round. If something is green and smart then it is blue. Kind things are blue. Kind things are not nice. All round things are not green. Round, smart things are green. Nice, blue things are kind. All smart things are not kind. Rough things are smart.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is round.
("Gary" "is" "round" "+")
If something is green and smart then it is blue.
((("something" "is" "green" "+") ("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
Kind things are blue.
((("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
Kind things are not nice.
((("something" "is" "kind" "+")) -> ("something" "is" "nice" "-"))
All round things are not green.
((("something" "is" "round" "+")) -> ("something" "is" "green" "-"))
Round, smart things are green.
((("something" "is" "round" "+") ("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
Nice, blue things are kind.
((("something" "is" "nice" "+") ("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
All smart things are not kind.
((("something" "is" "smart" "+")) -> ("something" "is" "kind" "-"))
Rough things are smart.
((("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
Gary is round.
True
1
proof
[(triple7)]
("Gary" "is" "round" "+")
triple7
Bob is not rough.
False
1
inv-proof
[(triple2)]
("Bob" "is" "rough" "-")
triple2
Erin is not kind.
True
2
proof
[(((triple4) -> rule7))]
("Erin" "is" "kind" "-")
((triple4) -> (rule7 % int1))
Erin is not kind.
("Erin" "is" "kind" "-")
int1
Gary is green.
False
2
inv-proof
[(((triple7) -> rule4))]
("Gary" "is" "green" "+")
((triple7) -> (rule4 % int1))
Gary is not green.
("Gary" "is" "green" "-")
int1
Bob is not kind.
True
3
proof
[(((((triple2) -> rule8)) -> rule7))]
("Bob" "is" "kind" "-")
((((triple2) -> (rule8 % int2))) -> (rule7 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is kind.
False
3
inv-proof
[(((((triple2) -> rule8)) -> rule7))]
("Bob" "is" "kind" "+")
((((triple2) -> (rule8 % int2))) -> (rule7 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Fiona is not smart.
Unknown
inv-rconc
[@1: Fiona is smart.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Fiona" "is" "smart" "-")
Fiona is green.
Unknown
rconc
[@1: Fiona is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "green" "+")
Erin is not green.
Unknown
inv-rconc
[@1: Erin is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "green" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
Fiona is not nice.
Unknown
inv-random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "-")
Erin is nice.
Unknown
random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "+")
@0: Bob is blue.[(triple1)] Bob is rough.[(triple2)] Erin is blue.[(triple3)] Erin is smart.[(triple4)] Fiona is blue.[(triple5)] Gary is nice.[(triple6)] Gary is round.[(triple7)] @1: Bob is smart.[(((triple2) -> rule8))] Erin is not kind.[(((triple4) -> rule7))] Gary is not green.[(((triple7) -> rule4))] @2: Bob is not kind.[(((((triple2) -> rule8)) -> rule7))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Erin is blue.
("Erin" "is" "blue" "+")
triple3
Erin is smart.
("Erin" "is" "smart" "+")
triple4
Fiona is blue.
("Fiona" "is" "blue" "+")
triple5
Gary is nice.
("Gary" "is" "nice" "+")
triple6
Gary is round.
("Gary" "is" "round" "+")
triple7
Bob is smart.
("Bob" "is" "smart" "+")
((triple2) -> (rule8 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Erin is not kind.
("Erin" "is" "kind" "-")
((triple4) -> (rule7 % int1))
Erin is not kind.
("Erin" "is" "kind" "-")
int1
Gary is not green.
("Gary" "is" "green" "-")
((triple7) -> (rule4 % int1))
Gary is not green.
("Gary" "is" "green" "-")
int1
Bob is not kind.
("Bob" "is" "kind" "-")
((((triple2) -> (rule8 % int2))) -> (rule7 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2