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