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