Bob is kind. Charlie is round. Erin is green. Smart people are green. All kind people are young. Quiet, green people are not young. If someone is round then they are quiet. If someone is smart and green then they are quiet. If Charlie is round then Charlie is smart. If Charlie is kind and Charlie is quiet then Charlie is cold. If Erin is smart and Erin is round then Erin is not quiet.
Bob is kind.
("Bob" "is" "kind" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Erin is green.
("Erin" "is" "green" "+")
Smart people are green.
((("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
All kind people are young.
((("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
Quiet, green people are not young.
((("someone" "is" "quiet" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "young" "-"))
If someone is round then they are quiet.
((("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
If someone is smart and green then they are quiet.
((("someone" "is" "smart" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "quiet" "+"))
If Charlie is round then Charlie is smart.
((("Charlie" "is" "round" "+")) -> ("Charlie" "is" "smart" "+"))
If Charlie is kind and Charlie is quiet then Charlie is cold.
((("Charlie" "is" "kind" "+") ("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "cold" "+"))
If Erin is smart and Erin is round then Erin is not quiet.
((("Erin" "is" "smart" "+") ("Erin" "is" "round" "+")) -> ("Erin" "is" "quiet" "-"))
Bob is kind.
True
1
proof
[(triple1)]
("Bob" "is" "kind" "+")
triple1
Bob is not kind.
False
1
inv-proof
[(triple1)]
("Bob" "is" "kind" "-")
triple1
Bob is young.
True
2
proof
[(((triple1) -> rule2))]
("Bob" "is" "young" "+")
((triple1) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Charlie is not quiet.
False
2
inv-proof
[(((triple2) -> rule4) OR ((((triple2) -> rule6) ((((triple2) -> rule6)) -> rule1)) -> rule5))]
("Charlie" "is" "quiet" "-")
((triple2) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((((triple2) -> (rule6 % int3)) ((((triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is green.
True
3
proof
[(((((triple2) -> rule6)) -> rule1))]
("Charlie" "is" "green" "+")
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is not green.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule1))]
("Charlie" "is" "green" "-")
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is not young.
True
6
proof
[(((((triple2) -> rule4) ((((triple2) -> rule6)) -> rule1)) -> rule3) OR ((((((triple2) -> rule6) ((((triple2) -> rule6)) -> rule1)) -> rule5) ((((triple2) -> rule6)) -> rule1)) -> rule3))]
("Charlie" "is" "young" "-")
((((triple2) -> (rule4 % int4)) ((((triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
((((((triple2) -> (rule6 % int4)) ((((triple2) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule5 % int2)) ((((triple2) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule3 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
int4
Charlie is young.
False
6
inv-proof
[(((((triple2) -> rule4) ((((triple2) -> rule6)) -> rule1)) -> rule3) OR ((((((triple2) -> rule6) ((((triple2) -> rule6)) -> rule1)) -> rule5) ((((triple2) -> rule6)) -> rule1)) -> rule3))]
("Charlie" "is" "young" "+")
((((triple2) -> (rule4 % int4)) ((((triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
((((((triple2) -> (rule6 % int4)) ((((triple2) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule5 % int2)) ((((triple2) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule3 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
int4
Erin is not quiet.
Unknown
inv-rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "quiet" "-")
Erin is young.
Unknown
rconc
[@1: Erin is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "young" "+")
Bob is not green.
Unknown
inv-rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "green" "-")
Charlie is cold.
Unknown
rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Charlie" "is" "cold" "+")
Erin is not round.
Unknown
inv-random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
Bob is not smart.
Unknown
inv-random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
@0: Bob is kind.[(triple1)] Charlie is round.[(triple2)] Erin is green.[(triple3)] @1: Bob is young.[(((triple1) -> rule2))] Charlie is quiet.[(((triple2) -> rule4) OR ((((triple2) -> rule6) ((((triple2) -> rule6)) -> rule1)) -> rule5))] Charlie is smart.[(((triple2) -> rule6))] @2: Charlie is green.[(((((triple2) -> rule6)) -> rule1))] @3: Charlie is not young.[(((((triple2) -> rule4) ((((triple2) -> rule6)) -> rule1)) -> rule3) OR ((((((triple2) -> rule6) ((((triple2) -> rule6)) -> rule1)) -> rule5) ((((triple2) -> rule6)) -> rule1)) -> rule3))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Charlie is round.
("Charlie" "is" "round" "+")
triple2
Erin is green.
("Erin" "is" "green" "+")
triple3
Bob is young.
("Bob" "is" "young" "+")
((triple1) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple2) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((((triple2) -> (rule6 % int3)) ((((triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple2) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is not young.
("Charlie" "is" "young" "-")
((((triple2) -> (rule4 % int4)) ((((triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
((((((triple2) -> (rule6 % int4)) ((((triple2) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule5 % int2)) ((((triple2) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule3 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
int4