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