Anne is big. Anne is nice. Anne is quiet. Bob is nice. Dave is kind. Fiona is kind. Fiona is nice. If someone is quiet then they are nice. All furry people are nice. All nice people are furry. If someone is big then they are quiet. All nice people are big. If someone is smart then they are big. All kind people are smart. If someone is white then they are big.
Anne is big.
("Anne" "is" "big" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
If someone is quiet then they are nice.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
All furry people are nice.
((("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
All nice people are furry.
((("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "+"))
If someone is big then they are quiet.
((("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
All nice people are big.
((("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
If someone is smart then they are big.
((("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
All kind people are smart.
((("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
If someone is white then they are big.
((("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
Fiona is kind.
True
1
proof
[(triple6)]
("Fiona" "is" "kind" "+")
triple6
Anne is not big.
False
1
inv-proof
[(triple1 OR ((triple2) -> rule5) OR ((((triple3) -> rule1)) -> rule5))]
("Anne" "is" "big" "-")
triple1
((triple2) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Fiona is big.
True
2
proof
[(((triple7) -> rule5) OR ((((triple6) -> rule7)) -> rule6))]
("Fiona" "is" "big" "+")
((triple7) -> (rule5 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
((((triple6) -> (rule7 % int2))) -> (rule6 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Anne is not furry.
False
2
inv-proof
[(((triple2) -> rule3) OR ((((triple3) -> rule1)) -> rule3) OR ((((((triple1) -> rule4)) -> rule1)) -> rule3))]
("Anne" "is" "furry" "-")
((triple2) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
((((((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Dave is big.
True
3
proof
[(((((triple5) -> rule7)) -> rule6))]
("Dave" "is" "big" "+")
((((triple5) -> (rule7 % int2))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Bob is not quiet.
False
3
inv-proof
[(((((triple4) -> rule5)) -> rule4))]
("Bob" "is" "quiet" "-")
((((triple4) -> (rule5 % int2))) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Dave is quiet.
True
4
proof
[(((((((triple5) -> rule7)) -> rule6)) -> rule4))]
("Dave" "is" "quiet" "+")
((((((triple5) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is not quiet.
False
4
inv-proof
[(((((((triple5) -> rule7)) -> rule6)) -> rule4))]
("Dave" "is" "quiet" "-")
((((((triple5) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is nice.
True
5
proof
[(((((((((triple5) -> rule7)) -> rule6)) -> rule4)) -> rule1))]
("Dave" "is" "nice" "+")
((((((((triple5) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
Dave is not nice.
False
5
inv-proof
[(((((((((triple5) -> rule7)) -> rule6)) -> rule4)) -> rule1))]
("Dave" "is" "nice" "-")
((((((((triple5) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
Dave is furry.
True
6
proof
[(((((((((((triple5) -> rule7)) -> rule6)) -> rule4)) -> rule1)) -> rule3))]
("Dave" "is" "furry" "+")
((((((((((triple5) -> (rule7 % int5))) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
Dave is smart.
("Dave" "is" "smart" "+")
int5
Dave is not furry.
False
6
inv-proof
[(((((((((((triple5) -> rule7)) -> rule6)) -> rule4)) -> rule1)) -> rule3))]
("Dave" "is" "furry" "-")
((((((((((triple5) -> (rule7 % int5))) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
Dave is smart.
("Dave" "is" "smart" "+")
int5
Anne is not smart.
Unknown
inv-rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Anne" "is" "smart" "-")
Bob is smart.
Unknown
rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Bob" "is" "smart" "+")
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Fiona is white.
Unknown
random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "+")
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Anne is white.
Unknown
random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "+")
Bob is not white.
Unknown
inv-random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Anne is big.[(triple1 OR ((triple2) -> rule5) OR ((((triple3) -> rule1)) -> rule5))] Anne is nice.[(triple2 OR ((triple3) -> rule1) OR ((((triple1) -> rule4)) -> rule1))] Anne is quiet.[(triple3 OR ((triple1) -> rule4) OR ((((triple2) -> rule5)) -> rule4))] Bob is nice.[(triple4)] Dave is kind.[(triple5)] Fiona is kind.[(triple6)] Fiona is nice.[(triple7 OR ((((((((triple6) -> rule7)) -> rule6)) -> rule4)) -> rule1))] @1: Anne is furry.[(((triple2) -> rule3) OR ((((triple3) -> rule1)) -> rule3) OR ((((((triple1) -> rule4)) -> rule1)) -> rule3))] Bob is big.[(((triple4) -> rule5))] Bob is furry.[(((triple4) -> rule3))] Dave is smart.[(((triple5) -> rule7))] Fiona is big.[(((triple7) -> rule5) OR ((((triple6) -> rule7)) -> rule6))] Fiona is furry.[(((triple7) -> rule3) OR ((((((((((triple6) -> rule7)) -> rule6)) -> rule4)) -> rule1)) -> rule3))] Fiona is smart.[(((triple6) -> rule7))] @2: Bob is quiet.[(((((triple4) -> rule5)) -> rule4))] Dave is big.[(((((triple5) -> rule7)) -> rule6))] Fiona is quiet.[(((((triple7) -> rule5)) -> rule4) OR ((((((triple6) -> rule7)) -> rule6)) -> rule4))] @3: Dave is quiet.[(((((((triple5) -> rule7)) -> rule6)) -> rule4))] @4: Dave is nice.[(((((((((triple5) -> rule7)) -> rule6)) -> rule4)) -> rule1))] @5: Dave is furry.[(((((((((((triple5) -> rule7)) -> rule6)) -> rule4)) -> rule1)) -> rule3))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple2) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
triple2
((triple3) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
((triple1) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
triple4
Dave is kind.
("Dave" "is" "kind" "+")
triple5
Fiona is kind.
("Fiona" "is" "kind" "+")
triple6
Fiona is nice.
("Fiona" "is" "nice" "+")
triple7
((((((((triple6) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
int4
Anne is furry.
("Anne" "is" "furry" "+")
((triple2) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
((((((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
((triple4) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((triple4) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple5) -> (rule7 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((triple7) -> (rule5 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
((((triple6) -> (rule7 % int2))) -> (rule6 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
((triple7) -> (rule3 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((((((((((triple6) -> (rule7 % int5))) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is big.
("Fiona" "is" "big" "+")
int4
Fiona is smart.
("Fiona" "is" "smart" "+")
int5
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple6) -> (rule7 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((((triple4) -> (rule5 % int2))) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
((((triple5) -> (rule7 % int2))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((((triple7) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
((((((triple6) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
((((((triple5) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
((((((((triple5) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
Dave is furry.
("Dave" "is" "furry" "+")
((((((((((triple5) -> (rule7 % int5))) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
Dave is smart.
("Dave" "is" "smart" "+")
int5