Charlie is green. Charlie is smart. Dave is furry. Gary is furry. Gary is rough. Gary is smart. Harry is green. If Harry is furry then Harry is nice. If someone is nice then they are not blue. If someone is green then they are nice. If someone is smart and rough then they are nice. If Dave is round then Dave is not blue. If someone is rough and furry then they are smart. All nice people are furry. Round, furry people are rough. All green, furry people are round.
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is green.
("Harry" "is" "green" "+")
If Harry is furry then Harry is nice.
((("Harry" "is" "furry" "+")) -> ("Harry" "is" "nice" "+"))
If someone is nice then they are not blue.
((("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "-"))
If someone is green then they are nice.
((("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
If someone is smart and rough then they are nice.
((("someone" "is" "smart" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
If Dave is round then Dave is not blue.
((("Dave" "is" "round" "+")) -> ("Dave" "is" "blue" "-"))
If someone is rough and furry then they are smart.
((("someone" "is" "rough" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "+"))
All nice people are furry.
((("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "+"))
Round, furry people are rough.
((("someone" "is" "round" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
All green, furry people are round.
((("someone" "is" "green" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "round" "+"))
Gary is smart.
True
1
proof
[(triple6 OR ((triple5 triple4) -> rule6))]
("Gary" "is" "smart" "+")
triple6
((triple5 triple4) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is not furry.
False
1
inv-proof
[(triple4 OR ((((triple6 triple5) -> rule4)) -> rule7))]
("Gary" "is" "furry" "-")
triple4
((((triple6 triple5) -> (rule4 % int2))) -> (rule7 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is nice.
True
3
proof
[(((triple6 triple5) -> rule4) OR ((((triple5 triple4) -> rule6) triple5) -> rule4))]
("Gary" "is" "nice" "+")
((triple6 triple5) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((((triple5 triple4) -> (rule6 % int2)) triple5) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Harry is not nice.
False
2
inv-proof
[(((triple7) -> rule3))]
("Harry" "is" "nice" "-")
((triple7) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Charlie is not blue.
True
3
proof
[(((((triple1) -> rule3)) -> rule2))]
("Charlie" "is" "blue" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is not blue.
("Charlie" "is" "blue" "-")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is not furry.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule7))]
("Charlie" "is" "furry" "-")
((((triple1) -> (rule3 % int2))) -> (rule7 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is round.
True
5
proof
[(((triple1 ((((triple1) -> rule3)) -> rule7)) -> rule9))]
("Charlie" "is" "round" "+")
((triple1 ((((triple1) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule9 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is not round.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule3)) -> rule7)) -> rule9))]
("Charlie" "is" "round" "-")
((triple1 ((((triple1) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule9 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is rough.
True
9
proof
[(((((triple1 ((((triple1) -> rule3)) -> rule7)) -> rule9) ((((triple1) -> rule3)) -> rule7)) -> rule8))]
("Charlie" "is" "rough" "+")
((((triple1 ((((triple1) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule9 % int2)) ((((triple1) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule8 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
Harry is not rough.
False
9
inv-proof
[(((((triple7 ((((triple7) -> rule3)) -> rule7)) -> rule9) ((((triple7) -> rule3)) -> rule7)) -> rule8))]
("Harry" "is" "rough" "-")
((((triple7 ((((triple7) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule9 % int2)) ((((triple7) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule8 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
Harry is smart.
True
13
proof
[(((((((triple7 ((((triple7) -> rule3)) -> rule7)) -> rule9) ((((triple7) -> rule3)) -> rule7)) -> rule8) ((((triple7) -> rule3)) -> rule7)) -> rule6))]
("Harry" "is" "smart" "+")
((((((triple7 ((((triple7) -> (rule3 % int5))) -> (rule7 % int4))) -> (rule9 % int3)) ((((triple7) -> (rule3 % int5))) -> (rule7 % int4))) -> (rule8 % int2)) ((((triple7) -> (rule3 % int5))) -> (rule7 % int4))) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4
Harry is nice.
("Harry" "is" "nice" "+")
int5
Harry is not smart.
False
13
inv-proof
[(((((((triple7 ((((triple7) -> rule3)) -> rule7)) -> rule9) ((((triple7) -> rule3)) -> rule7)) -> rule8) ((((triple7) -> rule3)) -> rule7)) -> rule6))]
("Harry" "is" "smart" "-")
((((((triple7 ((((triple7) -> (rule3 % int5))) -> (rule7 % int4))) -> (rule9 % int3)) ((((triple7) -> (rule3 % int5))) -> (rule7 % int4))) -> (rule8 % int2)) ((((triple7) -> (rule3 % int5))) -> (rule7 % int4))) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4
Harry is nice.
("Harry" "is" "nice" "+")
int5
Gary is not round.
Unknown
inv-rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("Gary" "is" "round" "-")
Dave is smart.
Unknown
rconc
[@3: Dave is smart.[CWA. Example of deepest failure = (rule6 <- rule8 <- rule9 <- FAIL)]]
("Dave" "is" "smart" "+")
Dave is not round.
Unknown
inv-rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("Dave" "is" "round" "-")
Dave is nice.
Unknown
rconc
[@3: Dave is nice.[CWA. Example of deepest failure = (rule4 <- rule8 <- rule9 <- FAIL)]]
("Dave" "is" "nice" "+")
Dave is not rough.
Unknown
inv-rconc
[@2: Dave is rough.[CWA. Example of deepest failure = (rule8 <- rule9 <- FAIL)]]
("Dave" "is" "rough" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
@0: Charlie is green.[(triple1)] Charlie is smart.[(triple2 OR ((((((triple1 ((((triple1) -> rule3)) -> rule7)) -> rule9) ((((triple1) -> rule3)) -> rule7)) -> rule8) ((((triple1) -> rule3)) -> rule7)) -> rule6))] Dave is furry.[(triple3)] Gary is furry.[(triple4 OR ((((triple6 triple5) -> rule4)) -> rule7))] Gary is rough.[(triple5)] Gary is smart.[(triple6 OR ((triple5 triple4) -> rule6))] Harry is green.[(triple7)] @1: Charlie is nice.[(((triple1) -> rule3))] Gary is nice.[(((triple6 triple5) -> rule4) OR ((((triple5 triple4) -> rule6) triple5) -> rule4))] Harry is nice.[(((triple7) -> rule3))] @2: Charlie is furry.[(((((triple1) -> rule3)) -> rule7))] Charlie is not blue.[(((((triple1) -> rule3)) -> rule2))] Gary is not blue.[(((((triple6 triple5) -> rule4)) -> rule2) OR ((((((triple5 triple4) -> rule6) triple5) -> rule4)) -> rule2))] Harry is furry.[(((((triple7) -> rule3)) -> rule7))] Harry is not blue.[(((((triple7) -> rule3)) -> rule2))] @3: Charlie is round.[(((triple1 ((((triple1) -> rule3)) -> rule7)) -> rule9))] Harry is round.[(((triple7 ((((triple7) -> rule3)) -> rule7)) -> rule9))] @4: Charlie is rough.[(((((triple1 ((((triple1) -> rule3)) -> rule7)) -> rule9) ((((triple1) -> rule3)) -> rule7)) -> rule8))] Harry is rough.[(((((triple7 ((((triple7) -> rule3)) -> rule7)) -> rule9) ((((triple7) -> rule3)) -> rule7)) -> rule8))] @5: Harry is smart.[(((((((triple7 ((((triple7) -> rule3)) -> rule7)) -> rule9) ((((triple7) -> rule3)) -> rule7)) -> rule8) ((((triple7) -> rule3)) -> rule7)) -> rule6))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple2
((((((triple1 ((((triple1) -> (rule3 % int5))) -> (rule7 % int4))) -> (rule9 % int3)) ((((triple1) -> (rule3 % int5))) -> (rule7 % int4))) -> (rule8 % int2)) ((((triple1) -> (rule3 % int5))) -> (rule7 % int4))) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
int4
Charlie is nice.
("Charlie" "is" "nice" "+")
int5
Dave is furry.
("Dave" "is" "furry" "+")
triple3
Gary is furry.
("Gary" "is" "furry" "+")
triple4
((((triple6 triple5) -> (rule4 % int2))) -> (rule7 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
triple5
Gary is smart.
("Gary" "is" "smart" "+")
triple6
((triple5 triple4) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
triple7
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple1) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((triple6 triple5) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((((triple5 triple4) -> (rule6 % int2)) triple5) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((triple7) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((((triple1) -> (rule3 % int2))) -> (rule7 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is not blue.
("Charlie" "is" "blue" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is not blue.
("Charlie" "is" "blue" "-")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Gary is not blue.
("Gary" "is" "blue" "-")
((((triple6 triple5) -> (rule4 % int2))) -> (rule2 % int1))
Gary is not blue.
("Gary" "is" "blue" "-")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
((((((triple5 triple4) -> (rule6 % int3)) triple5) -> (rule4 % int2))) -> (rule2 % int1))
Gary is not blue.
("Gary" "is" "blue" "-")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
((((triple7) -> (rule3 % int2))) -> (rule7 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is not blue.
("Harry" "is" "blue" "-")
((((triple7) -> (rule3 % int2))) -> (rule2 % int1))
Harry is not blue.
("Harry" "is" "blue" "-")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
((triple1 ((((triple1) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule9 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
((triple7 ((((triple7) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule9 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple1 ((((triple1) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule9 % int2)) ((((triple1) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule8 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
Harry is rough.
("Harry" "is" "rough" "+")
((((triple7 ((((triple7) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule9 % int2)) ((((triple7) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule8 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
Harry is smart.
("Harry" "is" "smart" "+")
((((((triple7 ((((triple7) -> (rule3 % int5))) -> (rule7 % int4))) -> (rule9 % int3)) ((((triple7) -> (rule3 % int5))) -> (rule7 % int4))) -> (rule8 % int2)) ((((triple7) -> (rule3 % int5))) -> (rule7 % int4))) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4
Harry is nice.
("Harry" "is" "nice" "+")
int5