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