Anne is smart. Bob is furry. Erin is furry. Gary is young. Smart things are young. Kind, white things are young. If something is young then it is furry. If Anne is smart and Anne is furry then Anne is white. All white, young things are kind. All kind things are rough.
Anne is smart.
("Anne" "is" "smart" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Gary is young.
("Gary" "is" "young" "+")
Smart things are young.
((("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
Kind, white things are young.
((("something" "is" "kind" "+") ("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
If something is young then it is furry.
((("something" "is" "young" "+")) -> ("something" "is" "furry" "+"))
If Anne is smart and Anne is furry then Anne is white.
((("Anne" "is" "smart" "+") ("Anne" "is" "furry" "+")) -> ("Anne" "is" "white" "+"))
All white, young things are kind.
((("something" "is" "white" "+") ("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
All kind things are rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
Erin is furry.
True
1
proof
[(triple3)]
("Erin" "is" "furry" "+")
triple3
Gary is not young.
False
1
inv-proof
[(triple4)]
("Gary" "is" "young" "-")
triple4
Anne is young.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "young" "+")
((triple1) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is not young.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "young" "-")
((triple1) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is furry.
True
3
proof
[(((((triple1) -> rule1)) -> rule3))]
("Anne" "is" "furry" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is not furry.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3))]
("Anne" "is" "furry" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is white.
True
5
proof
[(((triple1 ((((triple1) -> rule1)) -> rule3)) -> rule4))]
("Anne" "is" "white" "+")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is not white.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule1)) -> rule3)) -> rule4))]
("Anne" "is" "white" "-")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Gary is not kind.
Unknown
inv-rconc
[@1: Gary is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "kind" "-")
Erin is rough.
Unknown
rconc
[@2: Erin is rough.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("Erin" "is" "rough" "+")
Erin is not young.
Unknown
inv-rconc
[@1: Erin is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "young" "-")
Erin is kind.
Unknown
rconc
[@1: Erin is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "kind" "+")
Gary is not smart.
Unknown
inv-random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "-")
Erin is white.
Unknown
random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "+")
Gary is not white.
Unknown
inv-random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
@0: Anne is smart.[(triple1)] Bob is furry.[(triple2)] Erin is furry.[(triple3)] Gary is young.[(triple4)] @1: Anne is young.[(((triple1) -> rule1))] Gary is furry.[(((triple4) -> rule3))] @2: Anne is furry.[(((((triple1) -> rule1)) -> rule3))] @3: Anne is white.[(((triple1 ((((triple1) -> rule1)) -> rule3)) -> rule4))] @4: Anne is kind.[(((((triple1 ((((triple1) -> rule1)) -> rule3)) -> rule4) ((triple1) -> rule1)) -> rule5))] @5: Anne is rough.[(((((((triple1 ((((triple1) -> rule1)) -> rule3)) -> rule4) ((triple1) -> rule1)) -> rule5)) -> rule6))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Erin is furry.
("Erin" "is" "furry" "+")
triple3
Gary is young.
("Gary" "is" "young" "+")
triple4
Anne is young.
("Anne" "is" "young" "+")
((triple1) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((triple4) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
((((triple1 ((((triple1) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule4 % int2)) ((triple1) -> (rule1 % int4))) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is rough.
("Anne" "is" "rough" "+")
((((((triple1 ((((triple1) -> (rule1 % int5))) -> (rule3 % int4))) -> (rule4 % int3)) ((triple1) -> (rule1 % int5))) -> (rule5 % int2))) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
Anne is young.
("Anne" "is" "young" "+")
int5