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