Bob is kind. Bob is smart. Charlie is kind. Charlie is red. Erin is blue. Erin is red. Gary is not green. Gary is kind. Gary is quiet. Gary is red. Gary is round. Gary is not smart. Quiet people are not green. If someone is red and round then they are kind. If Gary is smart then Gary is green. If Charlie is blue and Charlie is not green then Charlie is red. If someone is blue then they are smart. Kind, green people are smart.
Bob is kind.
("Bob" "is" "kind" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is red.
("Erin" "is" "red" "+")
Gary is not green.
("Gary" "is" "green" "-")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is not smart.
("Gary" "is" "smart" "-")
Quiet people are not green.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "-"))
If someone is red and round then they are kind.
((("someone" "is" "red" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
If Gary is smart then Gary is green.
((("Gary" "is" "smart" "+")) -> ("Gary" "is" "green" "+"))
If Charlie is blue and Charlie is not green then Charlie is red.
((("Charlie" "is" "blue" "+") ("Charlie" "is" "green" "~")) -> ("Charlie" "is" "red" "+"))
If someone is blue then they are smart.
((("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
Kind, green people are smart.
((("someone" "is" "kind" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "smart" "+"))
Gary is red.
True
1
proof
[(triple10)]
("Gary" "is" "red" "+")
triple10
Bob is not smart.
False
1
inv-proof
[(triple2)]
("Bob" "is" "smart" "-")
triple2
Erin is smart.
True
2
proof
[(((triple5) -> rule5))]
("Erin" "is" "smart" "+")
((triple5) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is not smart.
False
2
inv-proof
[(((triple5) -> rule5))]
("Erin" "is" "smart" "-")
((triple5) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is not kind.
Unknown
inv-rconc
[@1: Erin is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "kind" "-")
Charlie is smart.
Unknown
rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "smart" "+")
Erin is not quiet.
Unknown
inv-random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
@0: Bob is kind.[(triple1)] Bob is smart.[(triple2)] Charlie is kind.[(triple3)] Charlie is red.[(triple4)] Erin is blue.[(triple5)] Erin is red.[(triple6)] Gary is kind.[(triple8 OR ((triple10 triple11) -> rule2))] Gary is not green.[(triple7 OR ((triple9) -> rule1))] Gary is not smart.[(triple12)] Gary is quiet.[(triple9)] Gary is red.[(triple10)] Gary is round.[(triple11)] @1: Erin is smart.[(((triple5) -> rule5))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Charlie is red.
("Charlie" "is" "red" "+")
triple4
Erin is blue.
("Erin" "is" "blue" "+")
triple5
Erin is red.
("Erin" "is" "red" "+")
triple6
Gary is kind.
("Gary" "is" "kind" "+")
triple8
((triple10 triple11) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is not green.
("Gary" "is" "green" "-")
triple7
((triple9) -> (rule1 % int1))
Gary is not green.
("Gary" "is" "green" "-")
int1
Gary is not smart.
("Gary" "is" "smart" "-")
triple12
Gary is quiet.
("Gary" "is" "quiet" "+")
triple9
Gary is red.
("Gary" "is" "red" "+")
triple10
Gary is round.
("Gary" "is" "round" "+")
triple11
Erin is smart.
("Erin" "is" "smart" "+")
((triple5) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1