Anne is red. Erin is not round. Harry is furry. If someone is furry then they are smart. If Erin is not red then Erin is not white. If Harry is smart then Harry is red. All round, white people are nice. If someone is red and furry then they are white. If someone is nice and not smart then they are white. All smart, furry people are round. If someone is furry and nice then they are round.
Anne is red.
("Anne" "is" "red" "+")
Erin is not round.
("Erin" "is" "round" "-")
Harry is furry.
("Harry" "is" "furry" "+")
If someone is furry then they are smart.
((("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "+"))
If Erin is not red then Erin is not white.
((("Erin" "is" "red" "~")) -> ("Erin" "is" "white" "-"))
If Harry is smart then Harry is red.
((("Harry" "is" "smart" "+")) -> ("Harry" "is" "red" "+"))
All round, white people are nice.
((("someone" "is" "round" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "nice" "+"))
If someone is red and furry then they are white.
((("someone" "is" "red" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
If someone is nice and not smart then they are white.
((("someone" "is" "nice" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "white" "+"))
All smart, furry people are round.
((("someone" "is" "smart" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "round" "+"))
If someone is furry and nice then they are round.
((("someone" "is" "furry" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
Anne is red.
True
1
proof
[(triple1)]
("Anne" "is" "red" "+")
triple1
Erin is round.
False
1
inv-proof
[(triple2)]
("Erin" "is" "round" "+")
triple2
Harry is smart.
True
2
proof
[(((triple3) -> rule1))]
("Harry" "is" "smart" "+")
((triple3) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is not smart.
False
2
inv-proof
[(((triple3) -> rule1))]
("Harry" "is" "smart" "-")
((triple3) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Erin is not white.
Unknown
inv-rconc
[@1: Erin is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "white" "-")
Erin is smart.
Unknown
rconc
[@1: Erin is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "smart" "+")
Anne is not furry.
Unknown
inv-random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
@0: Anne is red.[(triple1)] Erin is not round.[(triple2)] Harry is furry.[(triple3)] @1: Harry is smart.[(((triple3) -> rule1))] @2: Harry is red.[(((((triple3) -> rule1)) -> rule3))] Harry is round.[(((((triple3) -> rule1) triple3) -> rule7))] @3: Harry is white.[(((((((triple3) -> rule1)) -> rule3) triple3) -> rule5))] @4: Harry is nice.[(((((((triple3) -> rule1) triple3) -> rule7) ((((((triple3) -> rule1)) -> rule3) triple3) -> rule5)) -> rule4))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Erin is not round.
("Erin" "is" "round" "-")
triple2
Harry is furry.
("Harry" "is" "furry" "+")
triple3
Harry is smart.
("Harry" "is" "smart" "+")
((triple3) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((((triple3) -> (rule1 % int2)) triple3) -> (rule7 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
((((((triple3) -> (rule1 % int3))) -> (rule3 % int2)) triple3) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
((((((triple3) -> (rule1 % int5)) triple3) -> (rule7 % int4)) ((((((triple3) -> (rule1 % int5))) -> (rule3 % int3)) triple3) -> (rule5 % int2))) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
int4
Harry is smart.
("Harry" "is" "smart" "+")
int5