Anne is big. Charlie is young. Fiona is nice. If Charlie is quiet then Charlie is kind. All young things are quiet. If something is big then it is quiet. All young, kind things are smart. All nice things are big. Quiet, kind things are smart. All smart things are green. All young, big things are nice.
Anne is big.
("Anne" "is" "big" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
If Charlie is quiet then Charlie is kind.
((("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "kind" "+"))
All young things are quiet.
((("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
If something is big then it is quiet.
((("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
All young, kind things are smart.
((("something" "is" "young" "+") ("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
All nice things are big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
Quiet, kind things are smart.
((("something" "is" "quiet" "+") ("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
All smart things are green.
((("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
All young, big things are nice.
((("something" "is" "young" "+") ("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
Fiona is nice.
True
1
proof
[(triple3)]
("Fiona" "is" "nice" "+")
triple3
Anne is not big.
False
1
inv-proof
[(triple1)]
("Anne" "is" "big" "-")
triple1
Charlie is quiet.
True
2
proof
[(((triple2) -> rule2))]
("Charlie" "is" "quiet" "+")
((triple2) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Anne is not quiet.
False
2
inv-proof
[(((triple1) -> rule3))]
("Anne" "is" "quiet" "-")
((triple1) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Fiona is quiet.
True
3
proof
[(((((triple3) -> rule5)) -> rule3))]
("Fiona" "is" "quiet" "+")
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Charlie is not kind.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule1))]
("Charlie" "is" "kind" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is smart.
True
5
proof
[(((triple2 ((((triple2) -> rule2)) -> rule1)) -> rule4) OR ((((triple2) -> rule2) ((((triple2) -> rule2)) -> rule1)) -> rule6))]
("Charlie" "is" "smart" "+")
((triple2 ((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
((((triple2) -> (rule2 % int3)) ((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is not smart.
False
5
inv-proof
[(((triple2 ((((triple2) -> rule2)) -> rule1)) -> rule4) OR ((((triple2) -> rule2) ((((triple2) -> rule2)) -> rule1)) -> rule6))]
("Charlie" "is" "smart" "-")
((triple2 ((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
((((triple2) -> (rule2 % int3)) ((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Fiona is not smart.
Unknown
inv-rconc
[@1: Fiona is smart.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "smart" "-")
Anne is nice.
Unknown
rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Anne" "is" "nice" "+")
Fiona is not green.
Unknown
inv-rconc
[@2: Fiona is green.[CWA. Example of deepest failure = (rule7 <- rule4 <- FAIL)]]
("Fiona" "is" "green" "-")
Anne is smart.
Unknown
rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "smart" "+")
Anne is not young.
Unknown
inv-random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "-")
Fiona is young.
Unknown
random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "+")
Fiona is not kind.
Unknown
inv-random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
@0: Anne is big.[(triple1)] Charlie is young.[(triple2)] Fiona is nice.[(triple3)] @1: Anne is quiet.[(((triple1) -> rule3))] Charlie is quiet.[(((triple2) -> rule2))] Fiona is big.[(((triple3) -> rule5))] @2: Charlie is kind.[(((((triple2) -> rule2)) -> rule1))] Fiona is quiet.[(((((triple3) -> rule5)) -> rule3))] @3: Charlie is smart.[(((triple2 ((((triple2) -> rule2)) -> rule1)) -> rule4) OR ((((triple2) -> rule2) ((((triple2) -> rule2)) -> rule1)) -> rule6))] @4: Charlie is green.[(((((triple2 ((((triple2) -> rule2)) -> rule1)) -> rule4)) -> rule7) OR ((((((triple2) -> rule2) ((((triple2) -> rule2)) -> rule1)) -> rule6)) -> rule7))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Charlie is young.
("Charlie" "is" "young" "+")
triple2
Fiona is nice.
("Fiona" "is" "nice" "+")
triple3
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple2) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((triple3) -> (rule5 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple2 ((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
((((triple2) -> (rule2 % int3)) ((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
((((triple2 ((((triple2) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
((((((triple2) -> (rule2 % int4)) ((((triple2) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4