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