Charlie is not green. Charlie is kind. Charlie is rough. Charlie is round. Dave is not red. Dave is not rough. Dave is not round. Erin is young. Harry is green. Harry is red. Harry is round. Harry is smart. If something is red then it is not rough. Red, green things are smart. All rough, green things are not round. Smart things are red. Smart, red things are kind. If Erin is young then Erin is smart.
Charlie is not green.
("Charlie" "is" "green" "-")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Dave is not red.
("Dave" "is" "red" "-")
Dave is not rough.
("Dave" "is" "rough" "-")
Dave is not round.
("Dave" "is" "round" "-")
Erin is young.
("Erin" "is" "young" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If something is red then it is not rough.
((("something" "is" "red" "+")) -> ("something" "is" "rough" "-"))
Red, green things are smart.
((("something" "is" "red" "+") ("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
All rough, green things are not round.
((("something" "is" "rough" "+") ("something" "is" "green" "+")) -> ("something" "is" "round" "-"))
Smart things are red.
((("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
Smart, red things are kind.
((("something" "is" "smart" "+") ("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
If Erin is young then Erin is smart.
((("Erin" "is" "young" "+")) -> ("Erin" "is" "smart" "+"))
Harry is smart.
True
1
proof
[(triple12 OR ((triple10 triple9) -> rule2))]
("Harry" "is" "smart" "+")
triple12
((triple10 triple9) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is not round.
False
1
inv-proof
[(triple11)]
("Harry" "is" "round" "-")
triple11
Harry is not rough.
True
2
proof
[(((triple10) -> rule1) OR ((((triple12) -> rule4)) -> rule1))]
("Harry" "is" "rough" "-")
((triple10) -> (rule1 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
((((triple12) -> (rule4 % int2))) -> (rule1 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is rough.
False
2
inv-proof
[(((triple10) -> rule1) OR ((((triple12) -> rule4)) -> rule1))]
("Harry" "is" "rough" "+")
((triple10) -> (rule1 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
((((triple12) -> (rule4 % int2))) -> (rule1 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Erin is red.
True
3
proof
[(((((triple8) -> rule6)) -> rule4))]
("Erin" "is" "red" "+")
((((triple8) -> (rule6 % int2))) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is not red.
False
3
inv-proof
[(((((triple8) -> rule6)) -> rule4))]
("Erin" "is" "red" "-")
((((triple8) -> (rule6 % int2))) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is not rough.
True
4
proof
[(((((((triple8) -> rule6)) -> rule4)) -> rule1))]
("Erin" "is" "rough" "-")
((((((triple8) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is rough.
False
4
inv-proof
[(((((((triple8) -> rule6)) -> rule4)) -> rule1))]
("Erin" "is" "rough" "+")
((((((triple8) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Dave is not smart.
Unknown
inv-rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "smart" "-")
Charlie is smart.
Unknown
rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "smart" "+")
Dave is not kind.
Unknown
inv-rconc
[@1: Dave is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "kind" "-")
Charlie is red.
Unknown
rconc
[@2: Charlie is red.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("Charlie" "is" "red" "+")
Charlie is not young.
Unknown
inv-random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "-")
Erin is round.
Unknown
random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "+")
Dave is not young.
Unknown
inv-random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
@0: Charlie is kind.[(triple2)] Charlie is not green.[(triple1)] Charlie is rough.[(triple3)] Charlie is round.[(triple4)] Dave is not red.[(triple5)] Dave is not rough.[(triple6)] Dave is not round.[(triple7)] Erin is young.[(triple8)] Harry is green.[(triple9)] Harry is red.[(triple10 OR ((triple12) -> rule4))] Harry is round.[(triple11)] Harry is smart.[(triple12 OR ((triple10 triple9) -> rule2))] @1: Erin is smart.[(((triple8) -> rule6))] Harry is kind.[(((triple12 triple10) -> rule5) OR ((triple12 ((triple12) -> rule4)) -> rule5) OR ((((triple10 triple9) -> rule2) triple10) -> rule5) OR ((((triple10 triple9) -> rule2) ((triple12) -> rule4)) -> rule5))] Harry is not rough.[(((triple10) -> rule1) OR ((((triple12) -> rule4)) -> rule1))] @2: Erin is red.[(((((triple8) -> rule6)) -> rule4))] @3: Erin is kind.[(((((triple8) -> rule6) ((((triple8) -> rule6)) -> rule4)) -> rule5))] Erin is not rough.[(((((((triple8) -> rule6)) -> rule4)) -> rule1))]
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Charlie is not green.
("Charlie" "is" "green" "-")
triple1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple3
Charlie is round.
("Charlie" "is" "round" "+")
triple4
Dave is not red.
("Dave" "is" "red" "-")
triple5
Dave is not rough.
("Dave" "is" "rough" "-")
triple6
Dave is not round.
("Dave" "is" "round" "-")
triple7
Erin is young.
("Erin" "is" "young" "+")
triple8
Harry is green.
("Harry" "is" "green" "+")
triple9
Harry is red.
("Harry" "is" "red" "+")
triple10
((triple12) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple11
Harry is smart.
("Harry" "is" "smart" "+")
triple12
((triple10 triple9) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple8) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((triple12 triple10) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple12 ((triple12) -> (rule4 % int2))) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((((triple10 triple9) -> (rule2 % int2)) triple10) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((((triple10 triple9) -> (rule2 % int3)) ((triple12) -> (rule4 % int2))) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is not rough.
("Harry" "is" "rough" "-")
((triple10) -> (rule1 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
((((triple12) -> (rule4 % int2))) -> (rule1 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
((((triple8) -> (rule6 % int2))) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
((((triple8) -> (rule6 % int3)) ((((triple8) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is not rough.
("Erin" "is" "rough" "-")
((((((triple8) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3