Bob is big. Bob is green. Bob is quiet. Gary is big. Harry is big. Harry is blue. Harry is quiet. If Harry is blue and Harry is smart then Harry is red. Red things are smart. Furry things are quiet. If something is big then it is furry. If something is quiet then it is furry. Quiet, furry things are red. All big, smart things are red. Quiet things are smart.
Bob is big.
("Bob" "is" "big" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Gary is big.
("Gary" "is" "big" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
If Harry is blue and Harry is smart then Harry is red.
((("Harry" "is" "blue" "+") ("Harry" "is" "smart" "+")) -> ("Harry" "is" "red" "+"))
Red things are smart.
((("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
Furry things are quiet.
((("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
If something is big then it is furry.
((("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
If something is quiet then it is furry.
((("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
Quiet, furry things are red.
((("something" "is" "quiet" "+") ("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
All big, smart things are red.
((("something" "is" "big" "+") ("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
Quiet things are smart.
((("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
Harry is quiet.
True
1
proof
[(triple7 OR ((((triple5) -> rule4)) -> rule3))]
("Harry" "is" "quiet" "+")
triple7
((((triple5) -> (rule4 % int2))) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Bob is not green.
False
1
inv-proof
[(triple2)]
("Bob" "is" "green" "-")
triple2
Harry is furry.
True
2
proof
[(((triple5) -> rule4) OR ((triple7) -> rule5))]
("Harry" "is" "furry" "+")
((triple5) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((triple7) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Bob is not furry.
False
2
inv-proof
[(((triple1) -> rule4) OR ((triple3) -> rule5))]
("Bob" "is" "furry" "-")
((triple1) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((triple3) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Gary is quiet.
True
3
proof
[(((((triple4) -> rule4)) -> rule3))]
("Gary" "is" "quiet" "+")
((((triple4) -> (rule4 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is not quiet.
False
3
inv-proof
[(((((triple4) -> rule4)) -> rule3))]
("Gary" "is" "quiet" "-")
((((triple4) -> (rule4 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is smart.
True
4
proof
[(((((((triple4) -> rule4)) -> rule3)) -> rule8) OR ((((((((triple4) -> rule4)) -> rule3) ((triple4) -> rule4)) -> rule6)) -> rule2))]
("Gary" "is" "smart" "+")
((((((triple4) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
((((((((triple4) -> (rule4 % int4))) -> (rule3 % int3)) ((triple4) -> (rule4 % int4))) -> (rule6 % int2))) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
int4
Gary is not smart.
False
4
inv-proof
[(((((((triple4) -> rule4)) -> rule3)) -> rule8) OR ((((((((triple4) -> rule4)) -> rule3) ((triple4) -> rule4)) -> rule6)) -> rule2))]
("Gary" "is" "smart" "-")
((((((triple4) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
((((((((triple4) -> (rule4 % int4))) -> (rule3 % int3)) ((triple4) -> (rule4 % int4))) -> (rule6 % int2))) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
int4
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
@0: Bob is big.[(triple1)] Bob is green.[(triple2)] Bob is quiet.[(triple3 OR ((((triple1) -> rule4)) -> rule3))] Gary is big.[(triple4)] Harry is big.[(triple5)] Harry is blue.[(triple6)] Harry is quiet.[(triple7 OR ((((triple5) -> rule4)) -> rule3))] @1: Bob is furry.[(((triple1) -> rule4) OR ((triple3) -> rule5))] Bob is smart.[(((triple3) -> rule8) OR ((((((triple1) -> rule4)) -> rule3)) -> rule8) OR ((((triple3 ((triple1) -> rule4)) -> rule6)) -> rule2) OR ((((triple3 ((triple3) -> rule5)) -> rule6)) -> rule2) OR ((((((((triple1) -> rule4)) -> rule3) ((triple1) -> rule4)) -> rule6)) -> rule2) OR ((((((((triple1) -> rule4)) -> rule3) ((triple3) -> rule5)) -> rule6)) -> rule2))] Gary is furry.[(((triple4) -> rule4))] Harry is furry.[(((triple5) -> rule4) OR ((triple7) -> rule5))] Harry is smart.[(((triple7) -> rule8) OR ((((((triple5) -> rule4)) -> rule3)) -> rule8) OR ((((triple7 ((triple5) -> rule4)) -> rule6)) -> rule2) OR ((((triple7 ((triple7) -> rule5)) -> rule6)) -> rule2) OR ((((((((triple5) -> rule4)) -> rule3) ((triple5) -> rule4)) -> rule6)) -> rule2) OR ((((((((triple5) -> rule4)) -> rule3) ((triple7) -> rule5)) -> rule6)) -> rule2))] @2: Bob is red.[(((triple1 ((triple3) -> rule8)) -> rule7) OR ((triple3 ((triple1) -> rule4)) -> rule6) OR ((triple3 ((triple3) -> rule5)) -> rule6) OR ((((((triple1) -> rule4)) -> rule3) ((triple1) -> rule4)) -> rule6) OR ((((((triple1) -> rule4)) -> rule3) ((triple3) -> rule5)) -> rule6) OR ((triple1 ((((((triple1) -> rule4)) -> rule3)) -> rule8)) -> rule7))] Gary is quiet.[(((((triple4) -> rule4)) -> rule3))] Harry is red.[(((triple5 ((triple7) -> rule8)) -> rule7) OR ((triple6 ((triple7) -> rule8)) -> rule1) OR ((triple7 ((triple5) -> rule4)) -> rule6) OR ((triple7 ((triple7) -> rule5)) -> rule6) OR ((((((triple5) -> rule4)) -> rule3) ((triple5) -> rule4)) -> rule6) OR ((((((triple5) -> rule4)) -> rule3) ((triple7) -> rule5)) -> rule6) OR ((triple5 ((((((triple5) -> rule4)) -> rule3)) -> rule8)) -> rule7) OR ((triple6 ((((((triple5) -> rule4)) -> rule3)) -> rule8)) -> rule1))] @3: Gary is red.[(((((((triple4) -> rule4)) -> rule3) ((triple4) -> rule4)) -> rule6) OR ((triple4 ((((((triple4) -> rule4)) -> rule3)) -> rule8)) -> rule7))] Gary is smart.[(((((((triple4) -> rule4)) -> rule3)) -> rule8) OR ((((((((triple4) -> rule4)) -> rule3) ((triple4) -> rule4)) -> rule6)) -> rule2))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
triple4
Harry is big.
("Harry" "is" "big" "+")
triple5
Harry is blue.
("Harry" "is" "blue" "+")
triple6
Harry is quiet.
("Harry" "is" "quiet" "+")
triple7
((((triple5) -> (rule4 % int2))) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
((triple1) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((triple3) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((triple3) -> (rule8 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
((((triple3 ((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
((((triple3 ((triple3) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
((((((((triple1) -> (rule4 % int4))) -> (rule3 % int3)) ((triple1) -> (rule4 % int4))) -> (rule6 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
int4
((((((((triple1) -> (rule4 % int4))) -> (rule3 % int3)) ((triple3) -> (rule5 % int4))) -> (rule6 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
int4
Gary is furry.
("Gary" "is" "furry" "+")
((triple4) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((triple5) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((triple7) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple7) -> (rule8 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((((((triple5) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
((((triple7 ((triple5) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
((((triple7 ((triple7) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
((((((((triple5) -> (rule4 % int4))) -> (rule3 % int3)) ((triple5) -> (rule4 % int4))) -> (rule6 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4
((((((((triple5) -> (rule4 % int4))) -> (rule3 % int3)) ((triple7) -> (rule5 % int4))) -> (rule6 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4
Bob is red.
("Bob" "is" "red" "+")
((triple1 ((triple3) -> (rule8 % int2))) -> (rule7 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((triple3 ((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((triple3 ((triple3) -> (rule5 % int2))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((((triple1) -> (rule4 % int3))) -> (rule3 % int2)) ((triple1) -> (rule4 % int3))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
((((((triple1) -> (rule4 % int3))) -> (rule3 % int2)) ((triple3) -> (rule5 % int3))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
((triple1 ((((((triple1) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
int4
Gary is quiet.
("Gary" "is" "quiet" "+")
((((triple4) -> (rule4 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
((triple5 ((triple7) -> (rule8 % int2))) -> (rule7 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((triple6 ((triple7) -> (rule8 % int2))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((triple7 ((triple5) -> (rule4 % int2))) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((triple7 ((triple7) -> (rule5 % int2))) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((((triple5) -> (rule4 % int3))) -> (rule3 % int2)) ((triple5) -> (rule4 % int3))) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
((((((triple5) -> (rule4 % int3))) -> (rule3 % int2)) ((triple7) -> (rule5 % int3))) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
((triple5 ((((((triple5) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4
((triple6 ((((((triple5) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4
Gary is red.
("Gary" "is" "red" "+")
((((((triple4) -> (rule4 % int3))) -> (rule3 % int2)) ((triple4) -> (rule4 % int3))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
((triple4 ((((((triple4) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
int4
Gary is smart.
("Gary" "is" "smart" "+")
((((((triple4) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
((((((((triple4) -> (rule4 % int4))) -> (rule3 % int3)) ((triple4) -> (rule4 % int4))) -> (rule6 % int2))) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
int4