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