Anne is white. Charlie is quiet. All young, red things are quiet. If something is quiet and young then it is red. Furry, white things are young. If something is quiet and not furry then it is young. All quiet things are young. If Charlie is not young then Charlie is nice. If something is red and quiet then it is big. If something is nice then it is big.
Anne is white.
("Anne" "is" "white" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
All young, red things are quiet.
((("something" "is" "young" "+") ("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
If something is quiet and young then it is red.
((("something" "is" "quiet" "+") ("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
Furry, white things are young.
((("something" "is" "furry" "+") ("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
If something is quiet and not furry then it is young.
((("something" "is" "quiet" "+") ("something" "is" "furry" "~")) -> ("something" "is" "young" "+"))
All quiet things are young.
((("something" "is" "quiet" "+")) -> ("something" "is" "young" "+"))
If Charlie is not young then Charlie is nice.
((("Charlie" "is" "young" "~")) -> ("Charlie" "is" "nice" "+"))
If something is red and quiet then it is big.
((("something" "is" "red" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
If something is nice then it is big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
Anne is white.
True
1
proof
[(triple1)]
("Anne" "is" "white" "+")
triple1
Charlie is not quiet.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "quiet" "-")
triple2
Charlie is young.
True
2
proof
[(((triple2) -> rule5))]
("Charlie" "is" "young" "+")
((triple2) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is not young.
False
2
inv-proof
[(((triple2) -> rule5))]
("Charlie" "is" "young" "-")
((triple2) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is red.
True
4
proof
[(((triple2 ((triple2) -> rule5)) -> rule2))]
("Charlie" "is" "red" "+")
((triple2 ((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is not red.
False
4
inv-proof
[(((triple2 ((triple2) -> rule5)) -> rule2))]
("Charlie" "is" "red" "-")
((triple2 ((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is big.
True
6
proof
[(((((triple2 ((triple2) -> rule5)) -> rule2) triple2) -> rule7))]
("Charlie" "is" "big" "+")
((((triple2 ((triple2) -> (rule5 % int3))) -> (rule2 % int2)) triple2) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is not big.
False
6
inv-proof
[(((((triple2 ((triple2) -> rule5)) -> rule2) triple2) -> rule7))]
("Charlie" "is" "big" "-")
((((triple2 ((triple2) -> (rule5 % int3))) -> (rule2 % int2)) triple2) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is not nice.
Unknown
inv-rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "nice" "-")
Anne is red.
Unknown
rconc
[@2: Anne is red.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Anne" "is" "red" "+")
Anne is not quiet.
Unknown
inv-rconc
[@2: Anne is quiet.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Anne" "is" "quiet" "-")
Anne is young.
Unknown
rconc
[@3: Anne is young.[CWA. Example of deepest failure = (rule5 <- rule1 <- rule3 <- FAIL)]]
("Anne" "is" "young" "+")
Anne is not nice.
Unknown
inv-random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
Charlie is not furry.
Unknown
inv-random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
@0: Anne is white.[(triple1)] Charlie is quiet.[(triple2)] @1: Charlie is young.[(((triple2) -> rule5))] @2: Charlie is red.[(((triple2 ((triple2) -> rule5)) -> rule2))] @3: Charlie is big.[(((((triple2 ((triple2) -> rule5)) -> rule2) triple2) -> rule7))]
Anne is white.
("Anne" "is" "white" "+")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
Charlie is young.
("Charlie" "is" "young" "+")
((triple2) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((triple2 ((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
((((triple2 ((triple2) -> (rule5 % int3))) -> (rule2 % int2)) triple2) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3