Anne is furry. Anne is red. Anne is smart. Bob is big. Bob is furry. Bob is smart. Bob is young. Erin is furry. Erin is red. Erin is smart. Erin is not young. Gary is big. Gary is not furry. Gary is quiet. Gary is white. Gary is young. If Anne is white then Anne is quiet. All furry things are white. All furry, young things are smart. If Anne is quiet then Anne is big. If Gary is young then Gary is big. Quiet, smart things are furry. All smart things are furry. If Anne is not furry then Anne is red.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is not young.
("Erin" "is" "young" "-")
Gary is big.
("Gary" "is" "big" "+")
Gary is not furry.
("Gary" "is" "furry" "-")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
If Anne is white then Anne is quiet.
((("Anne" "is" "white" "+")) -> ("Anne" "is" "quiet" "+"))
All furry things are white.
((("something" "is" "furry" "+")) -> ("something" "is" "white" "+"))
All furry, young things are smart.
((("something" "is" "furry" "+") ("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
If Anne is quiet then Anne is big.
((("Anne" "is" "quiet" "+")) -> ("Anne" "is" "big" "+"))
If Gary is young then Gary is big.
((("Gary" "is" "young" "+")) -> ("Gary" "is" "big" "+"))
Quiet, smart things are furry.
((("something" "is" "quiet" "+") ("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
All smart things are furry.
((("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
If Anne is not furry then Anne is red.
((("Anne" "is" "furry" "~")) -> ("Anne" "is" "red" "+"))
Anne is furry.
True
1
proof
[(triple1 OR ((triple3) -> rule7))]
("Anne" "is" "furry" "+")
triple1
((triple3) -> (rule7 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Bob is not furry.
False
1
inv-proof
[(triple5 OR ((triple6) -> rule7))]
("Bob" "is" "furry" "-")
triple5
((triple6) -> (rule7 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is white.
True
2
proof
[(((triple5) -> rule2) OR ((((triple6) -> rule7)) -> rule2))]
("Bob" "is" "white" "+")
((triple5) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((((triple6) -> (rule7 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is not white.
False
2
inv-proof
[(((triple5) -> rule2) OR ((((triple6) -> rule7)) -> rule2))]
("Bob" "is" "white" "-")
((triple5) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((((triple6) -> (rule7 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Anne is quiet.
True
3
proof
[(((((triple1) -> rule2)) -> rule1) OR ((((((triple3) -> rule7)) -> rule2)) -> rule1))]
("Anne" "is" "quiet" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
((((((triple3) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is not quiet.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule1) OR ((((((triple3) -> rule7)) -> rule2)) -> rule1))]
("Anne" "is" "quiet" "-")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
((((((triple3) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is big.
True
4
proof
[(((((((triple1) -> rule2)) -> rule1)) -> rule4) OR ((((((((triple3) -> rule7)) -> rule2)) -> rule1)) -> rule4))]
("Anne" "is" "big" "+")
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
((((((((triple3) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
Anne is not big.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule1)) -> rule4) OR ((((((((triple3) -> rule7)) -> rule2)) -> rule1)) -> rule4))]
("Anne" "is" "big" "-")
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
((((((((triple3) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
Gary is not smart.
Unknown
inv-rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "smart" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
Gary is not red.
Unknown
inv-random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
Anne is not young.
Unknown
inv-random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
@0: Anne is furry.[(triple1 OR ((triple3) -> rule7))] Anne is red.[(triple2)] Anne is smart.[(triple3)] Bob is big.[(triple4)] Bob is furry.[(triple5 OR ((triple6) -> rule7))] Bob is smart.[(triple6 OR ((triple5 triple7) -> rule3))] Bob is young.[(triple7)] Erin is furry.[(triple8 OR ((triple10) -> rule7))] Erin is not young.[(triple11)] Erin is red.[(triple9)] Erin is smart.[(triple10)] Gary is big.[(triple12 OR ((triple16) -> rule5))] Gary is not furry.[(triple13)] Gary is quiet.[(triple14)] Gary is white.[(triple15)] Gary is young.[(triple16)] @1: Anne is white.[(((triple1) -> rule2) OR ((((triple3) -> rule7)) -> rule2))] Bob is white.[(((triple5) -> rule2) OR ((((triple6) -> rule7)) -> rule2))] Erin is white.[(((triple8) -> rule2) OR ((((triple10) -> rule7)) -> rule2))] @2: Anne is quiet.[(((((triple1) -> rule2)) -> rule1) OR ((((((triple3) -> rule7)) -> rule2)) -> rule1))] @3: Anne is big.[(((((((triple1) -> rule2)) -> rule1)) -> rule4) OR ((((((((triple3) -> rule7)) -> rule2)) -> rule1)) -> rule4))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
((triple3) -> (rule7 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
triple2
Anne is smart.
("Anne" "is" "smart" "+")
triple3
Bob is big.
("Bob" "is" "big" "+")
triple4
Bob is furry.
("Bob" "is" "furry" "+")
triple5
((triple6) -> (rule7 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
triple6
((triple5 triple7) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
triple7
Erin is furry.
("Erin" "is" "furry" "+")
triple8
((triple10) -> (rule7 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is not young.
("Erin" "is" "young" "-")
triple11
Erin is red.
("Erin" "is" "red" "+")
triple9
Erin is smart.
("Erin" "is" "smart" "+")
triple10
Gary is big.
("Gary" "is" "big" "+")
triple12
((triple16) -> (rule5 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is not furry.
("Gary" "is" "furry" "-")
triple13
Gary is quiet.
("Gary" "is" "quiet" "+")
triple14
Gary is white.
("Gary" "is" "white" "+")
triple15
Gary is young.
("Gary" "is" "young" "+")
triple16
Anne is white.
("Anne" "is" "white" "+")
((triple1) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((((triple3) -> (rule7 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
((triple5) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((((triple6) -> (rule7 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
((triple8) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((((triple10) -> (rule7 % int2))) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
((((((triple3) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
((((((((triple3) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4