Anne is big. Anne is quiet. Anne is round. Anne is smart. Anne is white. Anne is young. Charlie is big. Charlie is round. Charlie is white. Erin is kind. Erin is quiet. Erin is young. All big people are smart. If someone is big then they are smart. All white people are big.
Anne is big.
("Anne" "is" "big" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is young.
("Erin" "is" "young" "+")
All big people are smart.
((("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
If someone is big then they are smart.
((("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
All white people are big.
((("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
Anne is smart.
True
1
proof
[(triple4 OR ((triple1) -> rule1) OR ((triple1) -> rule2) OR ((((triple5) -> rule3)) -> rule1) OR ((((triple5) -> rule3)) -> rule2))]
("Anne" "is" "smart" "+")
triple4
((triple1) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((triple1) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
((((triple5) -> (rule3 % int2))) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Charlie is not round.
False
1
inv-proof
[(triple8)]
("Charlie" "is" "round" "-")
triple8
Charlie is smart.
True
2
proof
[(((triple7) -> rule1) OR ((triple7) -> rule2) OR ((((triple9) -> rule3)) -> rule1) OR ((((triple9) -> rule3)) -> rule2))]
("Charlie" "is" "smart" "+")
((triple7) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((triple7) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((((triple9) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((triple9) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is not smart.
False
2
inv-proof
[(((triple7) -> rule1) OR ((triple7) -> rule2) OR ((((triple9) -> rule3)) -> rule1) OR ((((triple9) -> rule3)) -> rule2))]
("Charlie" "is" "smart" "-")
((triple7) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((triple7) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((((triple9) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((triple9) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Erin is not smart.
Unknown
inv-rconc
[@2: Erin is smart.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Erin" "is" "smart" "-")
Erin is big.
Unknown
rconc
[@1: Erin is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "big" "+")
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Erin is round.
Unknown
random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "+")
@0: Anne is big.[(triple1 OR ((triple5) -> rule3))] Anne is quiet.[(triple2)] Anne is round.[(triple3)] Anne is smart.[(triple4 OR ((triple1) -> rule1) OR ((triple1) -> rule2) OR ((((triple5) -> rule3)) -> rule1) OR ((((triple5) -> rule3)) -> rule2))] Anne is white.[(triple5)] Anne is young.[(triple6)] Charlie is big.[(triple7 OR ((triple9) -> rule3))] Charlie is round.[(triple8)] Charlie is white.[(triple9)] Erin is kind.[(triple10)] Erin is quiet.[(triple11)] Erin is young.[(triple12)] @1: Charlie is smart.[(((triple7) -> rule1) OR ((triple7) -> rule2) OR ((((triple9) -> rule3)) -> rule1) OR ((((triple9) -> rule3)) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple5) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Anne is round.
("Anne" "is" "round" "+")
triple3
Anne is smart.
("Anne" "is" "smart" "+")
triple4
((triple1) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((triple1) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
((((triple5) -> (rule3 % int2))) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
triple5
Anne is young.
("Anne" "is" "young" "+")
triple6
Charlie is big.
("Charlie" "is" "big" "+")
triple7
((triple9) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
triple8
Charlie is white.
("Charlie" "is" "white" "+")
triple9
Erin is kind.
("Erin" "is" "kind" "+")
triple10
Erin is quiet.
("Erin" "is" "quiet" "+")
triple11
Erin is young.
("Erin" "is" "young" "+")
triple12
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple7) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((triple7) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((((triple9) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((triple9) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2