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