Anne is red. Harry is white. All quiet people are red. Big, round people are red. If someone is white then they are big. If Harry is round and Harry is big then Harry is red. If someone is big then they are round. If someone is quiet and not round then they are young.
Anne is red.
("Anne" "is" "red" "+")
Harry is white.
("Harry" "is" "white" "+")
All quiet people are red.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "+"))
Big, round people are red.
((("someone" "is" "big" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
If someone is white then they are big.
((("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
If Harry is round and Harry is big then Harry is red.
((("Harry" "is" "round" "+") ("Harry" "is" "big" "+")) -> ("Harry" "is" "red" "+"))
If someone is big then they are round.
((("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
If someone is quiet and not round then they are young.
((("someone" "is" "quiet" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "young" "+"))
Anne is red.
True
1
proof
[(triple1)]
("Anne" "is" "red" "+")
triple1
Harry is not white.
False
1
inv-proof
[(triple2)]
("Harry" "is" "white" "-")
triple2
Harry is big.
True
2
proof
[(((triple2) -> rule3))]
("Harry" "is" "big" "+")
((triple2) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is not big.
False
2
inv-proof
[(((triple2) -> rule3))]
("Harry" "is" "big" "-")
((triple2) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
True
3
proof
[(((((triple2) -> rule3)) -> rule5))]
("Harry" "is" "round" "+")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not round.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule5))]
("Harry" "is" "round" "-")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is red.
True
6
proof
[(((((triple2) -> rule3) ((((triple2) -> rule3)) -> rule5)) -> rule2) OR ((((((triple2) -> rule3)) -> rule5) ((triple2) -> rule3)) -> rule4))]
("Harry" "is" "red" "+")
((((triple2) -> (rule3 % int3)) ((((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
((((((triple2) -> (rule3 % int3))) -> (rule5 % int2)) ((triple2) -> (rule3 % int3))) -> (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 not red.
False
6
inv-proof
[(((((triple2) -> rule3) ((((triple2) -> rule3)) -> rule5)) -> rule2) OR ((((((triple2) -> rule3)) -> rule5) ((triple2) -> rule3)) -> rule4))]
("Harry" "is" "red" "-")
((((triple2) -> (rule3 % int3)) ((((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
((((((triple2) -> (rule3 % int3))) -> (rule5 % int2)) ((triple2) -> (rule3 % int3))) -> (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 not young.
Unknown
inv-rconc
[@1: Harry is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "young" "-")
Anne is big.
Unknown
rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "big" "+")
Anne is not young.
Unknown
inv-rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "young" "-")
Anne is round.
Unknown
rconc
[@2: Anne is round.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Anne" "is" "round" "+")
Harry is not quiet.
Unknown
inv-random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "-")
Anne is white.
Unknown
random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "+")
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
@0: Anne is red.[(triple1)] Harry is white.[(triple2)] @1: Harry is big.[(((triple2) -> rule3))] @2: Harry is round.[(((((triple2) -> rule3)) -> rule5))] @3: Harry is red.[(((((triple2) -> rule3) ((((triple2) -> rule3)) -> rule5)) -> rule2) OR ((((((triple2) -> rule3)) -> rule5) ((triple2) -> rule3)) -> rule4))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Harry is white.
("Harry" "is" "white" "+")
triple2
Harry is big.
("Harry" "is" "big" "+")
((triple2) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
((((triple2) -> (rule3 % int3)) ((((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
((((((triple2) -> (rule3 % int3))) -> (rule5 % int2)) ((triple2) -> (rule3 % int3))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3