Anne is kind. Anne is quiet. Anne is rough. Anne is smart. Erin is quiet. Erin is rough. Gary is furry. Gary is kind. Gary is quiet. Gary is red. Gary is rough. Gary is round. Harry is furry. Harry is round. Harry is smart. If Harry is quiet and Harry is rough then Harry is round. All quiet people are kind. Round people are smart. If someone is smart then they are rough. Round, rough people are kind. All red people are furry. If Gary is smart and Gary is furry then Gary is quiet. If someone is quiet then they are rough.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If Harry is quiet and Harry is rough then Harry is round.
((("Harry" "is" "quiet" "+") ("Harry" "is" "rough" "+")) -> ("Harry" "is" "round" "+"))
All quiet people are kind.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
Round people are smart.
((("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
If someone is smart then they are rough.
((("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
Round, rough people are kind.
((("someone" "is" "round" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
All red people are furry.
((("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
If Gary is smart and Gary is furry then Gary is quiet.
((("Gary" "is" "smart" "+") ("Gary" "is" "furry" "+")) -> ("Gary" "is" "quiet" "+"))
If someone is quiet then they are rough.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
Gary is quiet.
True
1
proof
[(triple9 OR ((((triple12) -> rule3) triple7) -> rule7) OR ((((triple12) -> rule3) ((triple10) -> rule6)) -> rule7))]
("Gary" "is" "quiet" "+")
triple9
((((triple12) -> (rule3 % int2)) triple7) -> (rule7 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
((((triple12) -> (rule3 % int3)) ((triple10) -> (rule6 % int2))) -> (rule7 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Anne is not kind.
False
1
inv-proof
[(triple1 OR ((triple2) -> rule2))]
("Anne" "is" "kind" "-")
triple1
((triple2) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Harry is rough.
True
2
proof
[(((triple15) -> rule4) OR ((((triple14) -> rule3)) -> rule4))]
("Harry" "is" "rough" "+")
((triple15) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple14) -> (rule3 % int2))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Erin is not kind.
False
2
inv-proof
[(((triple5) -> rule2))]
("Erin" "is" "kind" "-")
((triple5) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is not furry.
Unknown
inv-rconc
[@1: Erin is furry.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "furry" "-")
Anne is furry.
Unknown
rconc
[@1: Anne is furry.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "furry" "+")
Anne is not red.
Unknown
inv-random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
@0: Anne is kind.[(triple1 OR ((triple2) -> rule2))] Anne is quiet.[(triple2)] Anne is rough.[(triple3 OR ((triple2) -> rule8) OR ((triple4) -> rule4))] Anne is smart.[(triple4)] Erin is quiet.[(triple5)] Erin is rough.[(triple6 OR ((triple5) -> rule8))] Gary is furry.[(triple7 OR ((triple10) -> rule6))] Gary is kind.[(triple8 OR ((triple9) -> rule2) OR ((triple12 triple11) -> rule5) OR ((triple12 ((triple9) -> rule8)) -> rule5) OR ((((((triple12) -> rule3) triple7) -> rule7)) -> rule2) OR ((triple12 ((((triple12) -> rule3)) -> rule4)) -> rule5) OR ((((((triple12) -> rule3) ((triple10) -> rule6)) -> rule7)) -> rule2) OR ((triple12 ((((((triple12) -> rule3) triple7) -> rule7)) -> rule8)) -> rule5) OR ((triple12 ((((((triple12) -> rule3) ((triple10) -> rule6)) -> rule7)) -> rule8)) -> rule5))] Gary is quiet.[(triple9 OR ((((triple12) -> rule3) triple7) -> rule7) OR ((((triple12) -> rule3) ((triple10) -> rule6)) -> rule7))] Gary is red.[(triple10)] Gary is rough.[(triple11 OR ((triple9) -> rule8) OR ((((triple12) -> rule3)) -> rule4) OR ((((((triple12) -> rule3) triple7) -> rule7)) -> rule8) OR ((((((triple12) -> rule3) ((triple10) -> rule6)) -> rule7)) -> rule8))] Gary is round.[(triple12)] Harry is furry.[(triple13)] Harry is round.[(triple14)] Harry is smart.[(triple15 OR ((triple14) -> rule3))] @1: Erin is kind.[(((triple5) -> rule2))] Gary is smart.[(((triple12) -> rule3))] Harry is rough.[(((triple15) -> rule4) OR ((((triple14) -> rule3)) -> rule4))] @2: Harry is kind.[(((triple14 ((triple15) -> rule4)) -> rule5) OR ((triple14 ((((triple14) -> rule3)) -> rule4)) -> rule5))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
((triple2) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Anne is rough.
("Anne" "is" "rough" "+")
triple3
((triple2) -> (rule8 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((triple4) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
triple4
Erin is quiet.
("Erin" "is" "quiet" "+")
triple5
Erin is rough.
("Erin" "is" "rough" "+")
triple6
((triple5) -> (rule8 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
triple7
((triple10) -> (rule6 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
triple8
((triple9) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((triple12 triple11) -> (rule5 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((triple12 ((triple9) -> (rule8 % int2))) -> (rule5 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((((((triple12) -> (rule3 % int3)) triple7) -> (rule7 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
((triple12 ((((triple12) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
((((((triple12) -> (rule3 % int4)) ((triple10) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
((triple12 ((((((triple12) -> (rule3 % int4)) triple7) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
((triple12 ((((((triple12) -> (rule3 % int5)) ((triple10) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
int4
Gary is smart.
("Gary" "is" "smart" "+")
int5
Gary is quiet.
("Gary" "is" "quiet" "+")
triple9
((((triple12) -> (rule3 % int2)) triple7) -> (rule7 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
((((triple12) -> (rule3 % int3)) ((triple10) -> (rule6 % int2))) -> (rule7 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
triple10
Gary is rough.
("Gary" "is" "rough" "+")
triple11
((triple9) -> (rule8 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((((triple12) -> (rule3 % int2))) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
((((((triple12) -> (rule3 % int3)) triple7) -> (rule7 % int2))) -> (rule8 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
((((((triple12) -> (rule3 % int4)) ((triple10) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is round.
("Gary" "is" "round" "+")
triple12
Harry is furry.
("Harry" "is" "furry" "+")
triple13
Harry is round.
("Harry" "is" "round" "+")
triple14
Harry is smart.
("Harry" "is" "smart" "+")
triple15
((triple14) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((triple5) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple12) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple15) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple14) -> (rule3 % int2))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
((triple14 ((triple15) -> (rule4 % int2))) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((triple14 ((((triple14) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3