Anne is green. Harry is young. All quiet things are big. All young things are quiet. Big things are round. If something is young and round then it is red. All quiet things are red. If Harry is big and Harry is not quiet then Harry is not round.
Anne is green.
("Anne" "is" "green" "+")
Harry is young.
("Harry" "is" "young" "+")
All quiet things are big.
((("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
All young things are quiet.
((("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
Big things are round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
If something is young and round then it is red.
((("something" "is" "young" "+") ("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
All quiet things are red.
((("something" "is" "quiet" "+")) -> ("something" "is" "red" "+"))
If Harry is big and Harry is not quiet then Harry is not round.
((("Harry" "is" "big" "+") ("Harry" "is" "quiet" "~")) -> ("Harry" "is" "round" "-"))
Harry is young.
True
1
proof
[(triple2)]
("Harry" "is" "young" "+")
triple2
Anne is not green.
False
1
inv-proof
[(triple1)]
("Anne" "is" "green" "-")
triple1
Harry is quiet.
True
2
proof
[(((triple2) -> rule2))]
("Harry" "is" "quiet" "+")
((triple2) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is not quiet.
False
2
inv-proof
[(((triple2) -> rule2))]
("Harry" "is" "quiet" "-")
((triple2) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is red.
True
3
proof
[(((((triple2) -> rule2)) -> rule5) OR ((triple2 ((((((triple2) -> rule2)) -> rule1)) -> rule3)) -> rule4))]
("Harry" "is" "red" "+")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((triple2 ((((((triple2) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4
Harry is not red.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule5) OR ((triple2 ((((((triple2) -> rule2)) -> rule1)) -> rule3)) -> rule4))]
("Harry" "is" "red" "-")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((triple2 ((((((triple2) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4
Harry is round.
True
4
proof
[(((((((triple2) -> rule2)) -> rule1)) -> rule3))]
("Harry" "is" "round" "+")
((((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is not round.
False
4
inv-proof
[(((((((triple2) -> rule2)) -> rule1)) -> rule3))]
("Harry" "is" "round" "-")
((((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Anne is not quiet.
Unknown
inv-rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "quiet" "-")
Anne is big.
Unknown
rconc
[@2: Anne is big.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Anne" "is" "big" "+")
Anne is not red.
Unknown
inv-rconc
[@2: Anne is red.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("Anne" "is" "red" "-")
Anne is round.
Unknown
rconc
[@3: Anne is round.[CWA. Example of deepest failure = (rule3 <- rule1 <- rule2 <- FAIL)]]
("Anne" "is" "round" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Harry is rough.
Unknown
random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "+")
Anne is not young.
Unknown
inv-random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
@0: Anne is green.[(triple1)] Harry is young.[(triple2)] @1: Harry is quiet.[(((triple2) -> rule2))] @2: Harry is big.[(((((triple2) -> rule2)) -> rule1))] Harry is red.[(((((triple2) -> rule2)) -> rule5) OR ((triple2 ((((((triple2) -> rule2)) -> rule1)) -> rule3)) -> rule4))] @3: Harry is round.[(((((((triple2) -> rule2)) -> rule1)) -> rule3))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Harry is young.
("Harry" "is" "young" "+")
triple2
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple2) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((triple2 ((((((triple2) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4
Harry is round.
("Harry" "is" "round" "+")
((((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3