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