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