Charlie is blue. Charlie is quiet. Charlie is rough. Dave is rough. Erin is red. Harry is quiet. Harry is red. All red people are round. Kind people are rough. All quiet, blue people are kind. Blue people are kind. Round, red people are blue. If Erin is blue and Erin is rough then Erin is quiet. All smart people are blue. Quiet, smart people are red.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Erin is red.
("Erin" "is" "red" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
All red people are round.
((("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
Kind people are rough.
((("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
All quiet, blue people are kind.
((("someone" "is" "quiet" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
Blue people are kind.
((("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
Round, red people are blue.
((("someone" "is" "round" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
If Erin is blue and Erin is rough then Erin is quiet.
((("Erin" "is" "blue" "+") ("Erin" "is" "rough" "+")) -> ("Erin" "is" "quiet" "+"))
All smart people are blue.
((("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
Quiet, smart people are red.
((("someone" "is" "quiet" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
Charlie is quiet.
True
1
proof
[(triple2)]
("Charlie" "is" "quiet" "+")
triple2
Harry is not red.
False
1
inv-proof
[(triple7)]
("Harry" "is" "red" "-")
triple7
Harry is round.
True
2
proof
[(((triple7) -> rule1))]
("Harry" "is" "round" "+")
((triple7) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is not round.
False
2
inv-proof
[(((triple7) -> rule1))]
("Harry" "is" "round" "-")
((triple7) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is blue.
True
4
proof
[(((((triple7) -> rule1) triple7) -> rule5))]
("Harry" "is" "blue" "+")
((((triple7) -> (rule1 % int2)) triple7) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is not blue.
False
4
inv-proof
[(((((triple7) -> rule1) triple7) -> rule5))]
("Harry" "is" "blue" "-")
((((triple7) -> (rule1 % int2)) triple7) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is kind.
True
5
proof
[(((((((triple7) -> rule1) triple7) -> rule5)) -> rule4) OR ((triple6 ((((triple7) -> rule1) triple7) -> rule5)) -> rule3))]
("Harry" "is" "kind" "+")
((((((triple7) -> (rule1 % int3)) triple7) -> (rule5 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
((triple6 ((((triple7) -> (rule1 % int3)) triple7) -> (rule5 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is not kind.
False
5
inv-proof
[(((((((triple7) -> rule1) triple7) -> rule5)) -> rule4) OR ((triple6 ((((triple7) -> rule1) triple7) -> rule5)) -> rule3))]
("Harry" "is" "kind" "-")
((((((triple7) -> (rule1 % int3)) triple7) -> (rule5 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
((triple6 ((((triple7) -> (rule1 % int3)) triple7) -> (rule5 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is rough.
True
6
proof
[(((((((((triple7) -> rule1) triple7) -> rule5)) -> rule4)) -> rule2) OR ((((triple6 ((((triple7) -> rule1) triple7) -> rule5)) -> rule3)) -> rule2))]
("Harry" "is" "rough" "+")
((((((((triple7) -> (rule1 % int4)) triple7) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
int4
((((triple6 ((((triple7) -> (rule1 % int4)) triple7) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
int4
Harry is not rough.
False
6
inv-proof
[(((((((((triple7) -> rule1) triple7) -> rule5)) -> rule4)) -> rule2) OR ((((triple6 ((((triple7) -> rule1) triple7) -> rule5)) -> rule3)) -> rule2))]
("Harry" "is" "rough" "-")
((((((((triple7) -> (rule1 % int4)) triple7) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
int4
((((triple6 ((((triple7) -> (rule1 % int4)) triple7) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
int4
Erin is quiet.
True
11
proof
[(((((((triple5) -> rule1) triple5) -> rule5) ((((((((triple5) -> rule1) triple5) -> rule5)) -> rule4)) -> rule2)) -> rule6))]
("Erin" "is" "quiet" "+")
((((((triple5) -> (rule1 % int5)) triple5) -> (rule5 % int4)) ((((((((triple5) -> (rule1 % int5)) triple5) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
int4
Erin is round.
("Erin" "is" "round" "+")
int5
Erin is not quiet.
False
11
inv-proof
[(((((((triple5) -> rule1) triple5) -> rule5) ((((((((triple5) -> rule1) triple5) -> rule5)) -> rule4)) -> rule2)) -> rule6))]
("Erin" "is" "quiet" "-")
((((((triple5) -> (rule1 % int5)) triple5) -> (rule5 % int4)) ((((((((triple5) -> (rule1 % int5)) triple5) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
int4
Erin is round.
("Erin" "is" "round" "+")
int5
Dave is not red.
Unknown
inv-rconc
[@1: Dave is red.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Dave" "is" "red" "-")
Charlie is red.
Unknown
rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Charlie" "is" "red" "+")
Dave is not round.
Unknown
inv-rconc
[@2: Dave is round.[CWA. Example of deepest failure = (rule1 <- rule8 <- FAIL)]]
("Dave" "is" "round" "-")
Charlie is round.
Unknown
rconc
[@2: Charlie is round.[CWA. Example of deepest failure = (rule1 <- rule8 <- FAIL)]]
("Charlie" "is" "round" "+")
Dave is not blue.
Unknown
inv-rconc
[@2: Dave is blue.[CWA. Example of deepest failure = (rule5 <- rule8 <- FAIL)]]
("Dave" "is" "blue" "-")
Dave is kind.
Unknown
rconc
[@3: Dave is kind.[CWA. Example of deepest failure = (rule4 <- rule5 <- rule8 <- FAIL)]]
("Dave" "is" "kind" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
@0: Charlie is blue.[(triple1)] Charlie is quiet.[(triple2)] Charlie is rough.[(triple3 OR ((((triple1) -> rule4)) -> rule2) OR ((((triple2 triple1) -> rule3)) -> rule2))] Dave is rough.[(triple4)] Erin is red.[(triple5)] Harry is quiet.[(triple6)] Harry is red.[(triple7)] @1: Charlie is kind.[(((triple1) -> rule4) OR ((triple2 triple1) -> rule3))] Erin is round.[(((triple5) -> rule1))] Harry is round.[(((triple7) -> rule1))] @2: Erin is blue.[(((((triple5) -> rule1) triple5) -> rule5))] Harry is blue.[(((((triple7) -> rule1) triple7) -> rule5))] @3: Erin is kind.[(((((((triple5) -> rule1) triple5) -> rule5)) -> rule4))] Harry is kind.[(((((((triple7) -> rule1) triple7) -> rule5)) -> rule4) OR ((triple6 ((((triple7) -> rule1) triple7) -> rule5)) -> rule3))] @4: Erin is rough.[(((((((((triple5) -> rule1) triple5) -> rule5)) -> rule4)) -> rule2))] Harry is rough.[(((((((((triple7) -> rule1) triple7) -> rule5)) -> rule4)) -> rule2) OR ((((triple6 ((((triple7) -> rule1) triple7) -> rule5)) -> rule3)) -> rule2))] @5: Erin is quiet.[(((((((triple5) -> rule1) triple5) -> rule5) ((((((((triple5) -> rule1) triple5) -> rule5)) -> rule4)) -> rule2)) -> rule6))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple3
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((triple2 triple1) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
triple4
Erin is red.
("Erin" "is" "red" "+")
triple5
Harry is quiet.
("Harry" "is" "quiet" "+")
triple6
Harry is red.
("Harry" "is" "red" "+")
triple7
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple1) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((triple2 triple1) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
((triple5) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple7) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((((triple5) -> (rule1 % int2)) triple5) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
((((triple7) -> (rule1 % int2)) triple7) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
((((((triple5) -> (rule1 % int3)) triple5) -> (rule5 % int2))) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
((((((triple7) -> (rule1 % int3)) triple7) -> (rule5 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
((triple6 ((((triple7) -> (rule1 % int3)) triple7) -> (rule5 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
((((((((triple5) -> (rule1 % int4)) triple5) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
Harry is rough.
("Harry" "is" "rough" "+")
((((((((triple7) -> (rule1 % int4)) triple7) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
int4
((((triple6 ((((triple7) -> (rule1 % int4)) triple7) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
int4
Erin is quiet.
("Erin" "is" "quiet" "+")
((((((triple5) -> (rule1 % int5)) triple5) -> (rule5 % int4)) ((((((((triple5) -> (rule1 % int5)) triple5) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
int4
Erin is round.
("Erin" "is" "round" "+")
int5