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