Charlie is quiet. Charlie is red. Charlie is smart. Dave is blue. Dave is furry. Dave is green. Dave is kind. Dave is smart. Erin is furry. Erin is kind. If Dave is quiet then Dave is furry. If someone is furry then they are quiet. If someone is quiet and furry then they are smart. If Erin is furry then Erin is green. If someone is blue then they are red. If Charlie is quiet then Charlie is kind. If someone is smart and furry then they are kind. If Erin is smart and Erin is green then Erin is quiet.
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is kind.
("Erin" "is" "kind" "+")
If Dave is quiet then Dave is furry.
((("Dave" "is" "quiet" "+")) -> ("Dave" "is" "furry" "+"))
If someone is furry then they are quiet.
((("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
If someone is quiet and furry then they are smart.
((("someone" "is" "quiet" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "+"))
If Erin is furry then Erin is green.
((("Erin" "is" "furry" "+")) -> ("Erin" "is" "green" "+"))
If someone is blue then they are red.
((("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
If Charlie is quiet then Charlie is kind.
((("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "kind" "+"))
If someone is smart and furry then they are kind.
((("someone" "is" "smart" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
If Erin is smart and Erin is green then Erin is quiet.
((("Erin" "is" "smart" "+") ("Erin" "is" "green" "+")) -> ("Erin" "is" "quiet" "+"))
Erin is kind.
True
1
proof
[(triple10 OR ((((((triple9) -> rule2) triple9) -> rule3) triple9) -> rule7))]
("Erin" "is" "kind" "+")
triple10
((((((triple9) -> (rule2 % int3)) triple9) -> (rule3 % int2)) triple9) -> (rule7 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Dave is not smart.
False
1
inv-proof
[(triple8 OR ((((triple5) -> rule2) triple5) -> rule3))]
("Dave" "is" "smart" "-")
triple8
((((triple5) -> (rule2 % int2)) triple5) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Erin is not red.
Unknown
inv-rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "red" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
@0: Charlie is quiet.[(triple1)] Charlie is red.[(triple2)] Charlie is smart.[(triple3)] Dave is blue.[(triple4)] Dave is furry.[(triple5)] Dave is green.[(triple6)] Dave is kind.[(triple7 OR ((triple8 triple5) -> rule7) OR ((((((triple5) -> rule2) triple5) -> rule3) triple5) -> rule7))] Dave is smart.[(triple8 OR ((((triple5) -> rule2) triple5) -> rule3))] Erin is furry.[(triple9)] Erin is kind.[(triple10 OR ((((((triple9) -> rule2) triple9) -> rule3) triple9) -> rule7))] @1: Charlie is kind.[(((triple1) -> rule6))] Dave is quiet.[(((triple5) -> rule2))] Dave is red.[(((triple4) -> rule5))] Erin is green.[(((triple9) -> rule4))] Erin is quiet.[(((triple9) -> rule2))] @2: Erin is smart.[(((((triple9) -> rule2) triple9) -> rule3))]
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple1
Charlie is red.
("Charlie" "is" "red" "+")
triple2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple3
Dave is blue.
("Dave" "is" "blue" "+")
triple4
Dave is furry.
("Dave" "is" "furry" "+")
triple5
Dave is green.
("Dave" "is" "green" "+")
triple6
Dave is kind.
("Dave" "is" "kind" "+")
triple7
((triple8 triple5) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((((((triple5) -> (rule2 % int3)) triple5) -> (rule3 % int2)) triple5) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
triple8
((((triple5) -> (rule2 % int2)) triple5) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
triple9
Erin is kind.
("Erin" "is" "kind" "+")
triple10
((((((triple9) -> (rule2 % int3)) triple9) -> (rule3 % int2)) triple9) -> (rule7 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple1) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple5) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((triple4) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((triple9) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple9) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((((triple9) -> (rule2 % int2)) triple9) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2