Anne is kind. Anne is quiet. Bob is smart. Erin is blue. Erin is round. Erin is smart. Fiona is round. Big, blue things are smart. Big things are smart. If something is round then it is big. All round, kind things are white. Smart things are big. Round, white things are quiet. Smart things are kind. If Erin is kind and Erin is blue then Erin is big.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Big, blue things are smart.
((("something" "is" "big" "+") ("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
Big things are smart.
((("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
If something is round then it is big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
All round, kind things are white.
((("something" "is" "round" "+") ("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
Smart things are big.
((("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
Round, white things are quiet.
((("something" "is" "round" "+") ("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
Smart things are kind.
((("something" "is" "smart" "+")) -> ("something" "is" "kind" "+"))
If Erin is kind and Erin is blue then Erin is big.
((("Erin" "is" "kind" "+") ("Erin" "is" "blue" "+")) -> ("Erin" "is" "big" "+"))
Erin is smart.
True
1
proof
[(triple6 OR ((((triple5) -> rule3)) -> rule2) OR ((((triple5) -> rule3) triple4) -> rule1))]
("Erin" "is" "smart" "+")
triple6
((((triple5) -> (rule3 % int2))) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((((triple5) -> (rule3 % int2)) triple4) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is not round.
False
1
inv-proof
[(triple5)]
("Erin" "is" "round" "-")
triple5
Erin is big.
True
2
proof
[(((triple5) -> rule3) OR ((triple6) -> rule5) OR ((((triple6) -> rule7) triple4) -> rule8))]
("Erin" "is" "big" "+")
((triple5) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((triple6) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((((triple6) -> (rule7 % int2)) triple4) -> (rule8 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Fiona is not big.
False
2
inv-proof
[(((triple7) -> rule3))]
("Fiona" "is" "big" "-")
((triple7) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
True
3
proof
[(((((triple7) -> rule3)) -> rule2))]
("Fiona" "is" "smart" "+")
((((triple7) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is not smart.
False
3
inv-proof
[(((((triple7) -> rule3)) -> rule2))]
("Fiona" "is" "smart" "-")
((((triple7) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Erin is quiet.
True
6
proof
[(((triple5 ((triple5 ((triple6) -> rule7)) -> rule4)) -> rule6) OR ((triple5 ((triple5 ((((((triple5) -> rule3)) -> rule2)) -> rule7)) -> rule4)) -> rule6) OR ((triple5 ((triple5 ((((((triple5) -> rule3) triple4) -> rule1)) -> rule7)) -> rule4)) -> rule6))]
("Erin" "is" "quiet" "+")
((triple5 ((triple5 ((triple6) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((triple5 ((triple5 ((((((triple5) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Erin is big.
("Erin" "is" "big" "+")
int5
((triple5 ((triple5 ((((((triple5) -> (rule3 % int5)) triple4) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Erin is big.
("Erin" "is" "big" "+")
int5
Fiona is not kind.
False
4
inv-proof
[(((((((triple7) -> rule3)) -> rule2)) -> rule7))]
("Fiona" "is" "kind" "-")
((((((triple7) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is white.
True
6
proof
[(((triple7 ((((((triple7) -> rule3)) -> rule2)) -> rule7)) -> rule4))]
("Fiona" "is" "white" "+")
((triple7 ((((((triple7) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is big.
("Fiona" "is" "big" "+")
int4
Fiona is not white.
False
6
inv-proof
[(((triple7 ((((((triple7) -> rule3)) -> rule2)) -> rule7)) -> rule4))]
("Fiona" "is" "white" "-")
((triple7 ((((((triple7) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is big.
("Fiona" "is" "big" "+")
int4
Fiona is quiet.
True
8
proof
[(((triple7 ((triple7 ((((((triple7) -> rule3)) -> rule2)) -> rule7)) -> rule4)) -> rule6))]
("Fiona" "is" "quiet" "+")
((triple7 ((triple7 ((((((triple7) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
int4
Fiona is big.
("Fiona" "is" "big" "+")
int5
Fiona is not quiet.
False
8
inv-proof
[(((triple7 ((triple7 ((((((triple7) -> rule3)) -> rule2)) -> rule7)) -> rule4)) -> rule6))]
("Fiona" "is" "quiet" "-")
((triple7 ((triple7 ((((((triple7) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
int4
Fiona is big.
("Fiona" "is" "big" "+")
int5
Anne is not big.
Unknown
inv-rconc
[@3: Anne is big.[CWA. Example of deepest failure = (rule5 <- rule2 <- rule3 <- FAIL)]]
("Anne" "is" "big" "-")
Bob is white.
Unknown
rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "white" "+")
Bob is not quiet.
Unknown
inv-rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "quiet" "-")
Anne is smart.
Unknown
rconc
[@3: Anne is smart.[CWA. Example of deepest failure = (rule2 <- rule5 <- rule1 <- FAIL)]]
("Anne" "is" "smart" "+")
Anne is not white.
Unknown
inv-rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "white" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
Fiona is not blue.
Unknown
inv-random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
Anne is not round.
Unknown
inv-random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
@0: Anne is kind.[(triple1)] Anne is quiet.[(triple2)] Bob is smart.[(triple3)] Erin is blue.[(triple4)] Erin is round.[(triple5)] Erin is smart.[(triple6 OR ((((triple5) -> rule3)) -> rule2) OR ((((triple5) -> rule3) triple4) -> rule1))] Fiona is round.[(triple7)] @1: Bob is big.[(((triple3) -> rule5))] Bob is kind.[(((triple3) -> rule7))] Erin is big.[(((triple5) -> rule3) OR ((triple6) -> rule5) OR ((((triple6) -> rule7) triple4) -> rule8))] Erin is kind.[(((triple6) -> rule7) OR ((((((triple5) -> rule3)) -> rule2)) -> rule7) OR ((((((triple5) -> rule3) triple4) -> rule1)) -> rule7))] Fiona is big.[(((triple7) -> rule3))] @2: Erin is white.[(((triple5 ((triple6) -> rule7)) -> rule4) OR ((triple5 ((((((triple5) -> rule3)) -> rule2)) -> rule7)) -> rule4) OR ((triple5 ((((((triple5) -> rule3) triple4) -> rule1)) -> rule7)) -> rule4))] Fiona is smart.[(((((triple7) -> rule3)) -> rule2))] @3: Erin is quiet.[(((triple5 ((triple5 ((triple6) -> rule7)) -> rule4)) -> rule6) OR ((triple5 ((triple5 ((((((triple5) -> rule3)) -> rule2)) -> rule7)) -> rule4)) -> rule6) OR ((triple5 ((triple5 ((((((triple5) -> rule3) triple4) -> rule1)) -> rule7)) -> rule4)) -> rule6))] Fiona is kind.[(((((((triple7) -> rule3)) -> rule2)) -> rule7))] @4: Fiona is white.[(((triple7 ((((((triple7) -> rule3)) -> rule2)) -> rule7)) -> rule4))] @5: Fiona is quiet.[(((triple7 ((triple7 ((((((triple7) -> rule3)) -> rule2)) -> rule7)) -> rule4)) -> rule6))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Erin is blue.
("Erin" "is" "blue" "+")
triple4
Erin is round.
("Erin" "is" "round" "+")
triple5
Erin is smart.
("Erin" "is" "smart" "+")
triple6
((((triple5) -> (rule3 % int2))) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((((triple5) -> (rule3 % int2)) triple4) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
triple7
Bob is big.
("Bob" "is" "big" "+")
((triple3) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((triple3) -> (rule7 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((triple5) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((triple6) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((((triple6) -> (rule7 % int2)) triple4) -> (rule8 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
((triple6) -> (rule7 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((((((triple5) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
((((((triple5) -> (rule3 % int3)) triple4) -> (rule1 % int2))) -> (rule7 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Fiona is big.
("Fiona" "is" "big" "+")
((triple7) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple5 ((triple6) -> (rule7 % int2))) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((triple5 ((((((triple5) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4
((triple5 ((((((triple5) -> (rule3 % int4)) triple4) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4
Fiona is smart.
("Fiona" "is" "smart" "+")
((((triple7) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple5 ((triple5 ((triple6) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((triple5 ((triple5 ((((((triple5) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Erin is big.
("Erin" "is" "big" "+")
int5
((triple5 ((triple5 ((((((triple5) -> (rule3 % int5)) triple4) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Erin is big.
("Erin" "is" "big" "+")
int5
Fiona is kind.
("Fiona" "is" "kind" "+")
((((((triple7) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
((triple7 ((((((triple7) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is big.
("Fiona" "is" "big" "+")
int4
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple7 ((triple7 ((((((triple7) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
int4
Fiona is big.
("Fiona" "is" "big" "+")
int5