Anne is quiet. Charlie is young. Erin is cold. Harry is nice. Cold people are young. All cold people are young. All quiet, nice people are furry. If someone is furry then they are quiet. All round people are young. If someone is furry then they are young. All nice people are cold. Nice, young people are quiet.
Anne is quiet.
("Anne" "is" "quiet" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Cold people are young.
((("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
All cold people are young.
((("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
All quiet, nice people are furry.
((("someone" "is" "quiet" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "+"))
If someone is furry then they are quiet.
((("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
All round people are young.
((("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
If someone is furry then they are young.
((("someone" "is" "furry" "+")) -> ("someone" "is" "young" "+"))
All nice people are cold.
((("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
Nice, young people are quiet.
((("someone" "is" "nice" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "+"))
Anne is quiet.
True
1
proof
[(triple1)]
("Anne" "is" "quiet" "+")
triple1
Harry is not nice.
False
1
inv-proof
[(triple4)]
("Harry" "is" "nice" "-")
triple4
Erin is young.
True
2
proof
[(((triple3) -> rule1) OR ((triple3) -> rule2))]
("Erin" "is" "young" "+")
((triple3) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((triple3) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Harry is not cold.
False
2
inv-proof
[(((triple4) -> rule7))]
("Harry" "is" "cold" "-")
((triple4) -> (rule7 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is young.
True
3
proof
[(((((triple4) -> rule7)) -> rule1) OR ((((triple4) -> rule7)) -> rule2))]
("Harry" "is" "young" "+")
((((triple4) -> (rule7 % int2))) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((triple4) -> (rule7 % int2))) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is not young.
False
3
inv-proof
[(((((triple4) -> rule7)) -> rule1) OR ((((triple4) -> rule7)) -> rule2))]
("Harry" "is" "young" "-")
((((triple4) -> (rule7 % int2))) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((triple4) -> (rule7 % int2))) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is quiet.
True
5
proof
[(((triple4 ((((triple4) -> rule7)) -> rule1)) -> rule8) OR ((triple4 ((((triple4) -> rule7)) -> rule2)) -> rule8))]
("Harry" "is" "quiet" "+")
((triple4 ((((triple4) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
((triple4 ((((triple4) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is not quiet.
False
5
inv-proof
[(((triple4 ((((triple4) -> rule7)) -> rule1)) -> rule8) OR ((triple4 ((((triple4) -> rule7)) -> rule2)) -> rule8))]
("Harry" "is" "quiet" "-")
((triple4 ((((triple4) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
((triple4 ((((triple4) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Anne is not furry.
Unknown
inv-rconc
[@1: Anne is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "furry" "-")
Charlie is furry.
Unknown
rconc
[@1: Charlie is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "furry" "+")
Charlie is not quiet.
Unknown
inv-rconc
[@2: Charlie is quiet.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("Charlie" "is" "quiet" "-")
Anne is young.
Unknown
rconc
[@2: Anne is young.[CWA. Example of deepest failure = (rule1 <- rule7 <- FAIL)]]
("Anne" "is" "young" "+")
Harry is not round.
Unknown
inv-random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
Erin is not round.
Unknown
inv-random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
@0: Anne is quiet.[(triple1)] Charlie is young.[(triple2)] Erin is cold.[(triple3)] Harry is nice.[(triple4)] @1: Erin is young.[(((triple3) -> rule1) OR ((triple3) -> rule2))] Harry is cold.[(((triple4) -> rule7))] @2: Harry is young.[(((((triple4) -> rule7)) -> rule1) OR ((((triple4) -> rule7)) -> rule2))] @3: Harry is quiet.[(((triple4 ((((triple4) -> rule7)) -> rule1)) -> rule8) OR ((triple4 ((((triple4) -> rule7)) -> rule2)) -> rule8))] @4: Harry is furry.[(((((triple4 ((((triple4) -> rule7)) -> rule1)) -> rule8) triple4) -> rule3) OR ((((triple4 ((((triple4) -> rule7)) -> rule2)) -> rule8) triple4) -> rule3))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Charlie is young.
("Charlie" "is" "young" "+")
triple2
Erin is cold.
("Erin" "is" "cold" "+")
triple3
Harry is nice.
("Harry" "is" "nice" "+")
triple4
Erin is young.
("Erin" "is" "young" "+")
((triple3) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((triple3) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple4) -> (rule7 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((((triple4) -> (rule7 % int2))) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((triple4) -> (rule7 % int2))) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple4 ((((triple4) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
((triple4 ((((triple4) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
((((triple4 ((((triple4) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule8 % int2)) triple4) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
((((triple4 ((((triple4) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule8 % int2)) triple4) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4