Dave is green. Dave is smart. Erin is blue. Erin is red. Erin is round. Erin is not smart. Erin is not young. Gary is blue. Gary is red. Gary is round. If something is young then it is blue. If something is white and smart then it is round. If Dave is round then Dave is red. If something is blue then it is green. If something is red and smart then it is not green. Blue things are white. If something is smart and blue then it is young. Blue, green things are red.
Dave is green.
("Dave" "is" "green" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is not smart.
("Erin" "is" "smart" "-")
Erin is not young.
("Erin" "is" "young" "-")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
If something is young then it is blue.
((("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
If something is white and smart then it is round.
((("something" "is" "white" "+") ("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
If Dave is round then Dave is red.
((("Dave" "is" "round" "+")) -> ("Dave" "is" "red" "+"))
If something is blue then it is green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
If something is red and smart then it is not green.
((("something" "is" "red" "+") ("something" "is" "smart" "+")) -> ("something" "is" "green" "-"))
Blue things are white.
((("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
If something is smart and blue then it is young.
((("something" "is" "smart" "+") ("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
Blue, green things are red.
((("something" "is" "blue" "+") ("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
Gary is red.
True
1
proof
[(triple9 OR ((triple8 ((triple8) -> rule4)) -> rule8))]
("Gary" "is" "red" "+")
triple9
((triple8 ((triple8) -> (rule4 % int2))) -> (rule8 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is not blue.
False
1
inv-proof
[(triple8)]
("Gary" "is" "blue" "-")
triple8
Dave is not young.
Unknown
inv-rconc
[@2: Dave is young.[CWA. Example of deepest failure = (rule7 <- rule1 <- FAIL)]]
("Dave" "is" "young" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
@0: Dave is green.[(triple1)] Dave is smart.[(triple2)] Erin is blue.[(triple3)] Erin is not smart.[(triple6)] Erin is not young.[(triple7)] Erin is red.[(triple4 OR ((triple3 ((triple3) -> rule4)) -> rule8))] Erin is round.[(triple5)] Gary is blue.[(triple8)] Gary is red.[(triple9 OR ((triple8 ((triple8) -> rule4)) -> rule8))] Gary is round.[(triple10)] @1: Erin is green.[(((triple3) -> rule4))] Erin is white.[(((triple3) -> rule6))] Gary is green.[(((triple8) -> rule4))] Gary is white.[(((triple8) -> rule6))]
Dave is green.
("Dave" "is" "green" "+")
triple1
Dave is smart.
("Dave" "is" "smart" "+")
triple2
Erin is blue.
("Erin" "is" "blue" "+")
triple3
Erin is not smart.
("Erin" "is" "smart" "-")
triple6
Erin is not young.
("Erin" "is" "young" "-")
triple7
Erin is red.
("Erin" "is" "red" "+")
triple4
((triple3 ((triple3) -> (rule4 % int2))) -> (rule8 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
triple5
Gary is blue.
("Gary" "is" "blue" "+")
triple8
Gary is red.
("Gary" "is" "red" "+")
triple9
((triple8 ((triple8) -> (rule4 % int2))) -> (rule8 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
triple10
Erin is green.
("Erin" "is" "green" "+")
((triple3) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple3) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple8) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((triple8) -> (rule6 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1