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