Anne is big. Anne is green. Anne is not quiet. Anne is smart. Anne is young. Charlie is big. Charlie is green. Charlie is quiet. Charlie is smart. Erin is big. Erin is kind. Erin is quiet. Erin is smart. Erin is young. Fiona is not smart. Fiona is not young. If something is smart then it is round. Round things are kind. If Charlie is not big then Charlie is not quiet. If Anne is quiet and Anne is not round then Anne is young. If something is smart and not round then it is not quiet. If something is young and not big then it is quiet. If something is quiet and kind then it is young. If something is smart and not quiet then it is green.
Anne is big.
("Anne" "is" "big" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is not quiet.
("Anne" "is" "quiet" "-")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
Fiona is not smart.
("Fiona" "is" "smart" "-")
Fiona is not young.
("Fiona" "is" "young" "-")
If something is smart then it is round.
((("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
Round things are kind.
((("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
If Charlie is not big then Charlie is not quiet.
((("Charlie" "is" "big" "~")) -> ("Charlie" "is" "quiet" "-"))
If Anne is quiet and Anne is not round then Anne is young.
((("Anne" "is" "quiet" "+") ("Anne" "is" "round" "~")) -> ("Anne" "is" "young" "+"))
If something is smart and not round then it is not quiet.
((("something" "is" "smart" "+") ("something" "is" "round" "~")) -> ("something" "is" "quiet" "-"))
If something is young and not big then it is quiet.
((("something" "is" "young" "+") ("something" "is" "big" "~")) -> ("something" "is" "quiet" "+"))
If something is quiet and kind then it is young.
((("something" "is" "quiet" "+") ("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
If something is smart and not quiet then it is green.
((("something" "is" "smart" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "green" "+"))
Fiona is not smart.
True
1
proof
[(triple15)]
("Fiona" "is" "smart" "-")
triple15
Charlie is not big.
False
1
inv-proof
[(triple6)]
("Charlie" "is" "big" "-")
triple6
Erin is round.
True
2
proof
[(((triple13) -> rule1))]
("Erin" "is" "round" "+")
((triple13) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Charlie is not round.
False
2
inv-proof
[(((triple9) -> rule1))]
("Charlie" "is" "round" "-")
((triple9) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is kind.
True
3
proof
[(((((triple9) -> rule1)) -> rule2))]
("Charlie" "is" "kind" "+")
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Anne is not kind.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule2))]
("Anne" "is" "kind" "-")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Charlie is young.
True
5
proof
[(((triple8 ((((triple9) -> rule1)) -> rule2)) -> rule7))]
("Charlie" "is" "young" "+")
((triple8 ((((triple9) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is not young.
False
5
inv-proof
[(((triple8 ((((triple9) -> rule1)) -> rule2)) -> rule7))]
("Charlie" "is" "young" "-")
((triple8 ((((triple9) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Fiona is not round.
Unknown
inv-rconc
[@1: Fiona is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "round" "-")
Fiona is green.
Unknown
rconc
[@1: Fiona is green.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Fiona" "is" "green" "+")
Erin is not green.
Unknown
inv-rconc
[@1: Erin is green.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Erin" "is" "green" "-")
Fiona is kind.
Unknown
rconc
[@2: Fiona is kind.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Fiona" "is" "kind" "+")
@0: Anne is big.[(triple1)] Anne is green.[(triple2 OR ((triple4 triple3) -> rule8))] Anne is not quiet.[(triple3)] Anne is smart.[(triple4)] Anne is young.[(triple5)] Charlie is big.[(triple6)] Charlie is green.[(triple7)] Charlie is quiet.[(triple8)] Charlie is smart.[(triple9)] Erin is big.[(triple10)] Erin is kind.[(triple11 OR ((((triple13) -> rule1)) -> rule2))] Erin is quiet.[(triple12)] Erin is smart.[(triple13)] Erin is young.[(triple14 OR ((triple12 triple11) -> rule7) OR ((triple12 ((((triple13) -> rule1)) -> rule2)) -> rule7))] Fiona is not smart.[(triple15)] Fiona is not young.[(triple16)] @1: Anne is round.[(((triple4) -> rule1))] Charlie is round.[(((triple9) -> rule1))] Erin is round.[(((triple13) -> rule1))] @2: Anne is kind.[(((((triple4) -> rule1)) -> rule2))] Charlie is kind.[(((((triple9) -> rule1)) -> rule2))] @3: Charlie is young.[(((triple8 ((((triple9) -> rule1)) -> rule2)) -> rule7))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
((triple4 triple3) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is not quiet.
("Anne" "is" "quiet" "-")
triple3
Anne is smart.
("Anne" "is" "smart" "+")
triple4
Anne is young.
("Anne" "is" "young" "+")
triple5
Charlie is big.
("Charlie" "is" "big" "+")
triple6
Charlie is green.
("Charlie" "is" "green" "+")
triple7
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple8
Charlie is smart.
("Charlie" "is" "smart" "+")
triple9
Erin is big.
("Erin" "is" "big" "+")
triple10
Erin is kind.
("Erin" "is" "kind" "+")
triple11
((((triple13) -> (rule1 % int2))) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
triple12
Erin is smart.
("Erin" "is" "smart" "+")
triple13
Erin is young.
("Erin" "is" "young" "+")
triple14
((triple12 triple11) -> (rule7 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((triple12 ((((triple13) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Fiona is not smart.
("Fiona" "is" "smart" "-")
triple15
Fiona is not young.
("Fiona" "is" "young" "-")
triple16
Anne is round.
("Anne" "is" "round" "+")
((triple4) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((triple9) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
((triple13) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
((triple8 ((((triple9) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3