Anne is cold. Anne is not furry. Anne is quiet. Anne is not smart. Bob is round. Dave is cold. Dave is round. Dave is smart. Dave is young. Harry is furry. Harry is round. If Bob is green and Bob is round then Bob is furry. If someone is cold and round then they are smart. If Dave is furry then Dave is not quiet. If someone is green and young then they are quiet. If Anne is smart then Anne is not green. Quiet, round people are green. If someone is round then they are green. Furry people are young. Furry, quiet people are not cold.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is not furry.
("Anne" "is" "furry" "-")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is not smart.
("Anne" "is" "smart" "-")
Bob is round.
("Bob" "is" "round" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is round.
("Harry" "is" "round" "+")
If Bob is green and Bob is round then Bob is furry.
((("Bob" "is" "green" "+") ("Bob" "is" "round" "+")) -> ("Bob" "is" "furry" "+"))
If someone is cold and round then they are smart.
((("someone" "is" "cold" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
If Dave is furry then Dave is not quiet.
((("Dave" "is" "furry" "+")) -> ("Dave" "is" "quiet" "-"))
If someone is green and young then they are quiet.
((("someone" "is" "green" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "+"))
If Anne is smart then Anne is not green.
((("Anne" "is" "smart" "+")) -> ("Anne" "is" "green" "-"))
Quiet, round people are green.
((("someone" "is" "quiet" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
If someone is round then they are green.
((("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
Furry people are young.
((("someone" "is" "furry" "+")) -> ("someone" "is" "young" "+"))
Furry, quiet people are not cold.
((("someone" "is" "furry" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "-"))
Bob is round.
True
1
proof
[(triple5)]
("Bob" "is" "round" "+")
triple5
Bob is not round.
False
1
inv-proof
[(triple5)]
("Bob" "is" "round" "-")
triple5
Harry is young.
True
2
proof
[(((triple10) -> rule8))]
("Harry" "is" "young" "+")
((triple10) -> (rule8 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Bob is not green.
False
2
inv-proof
[(((triple5) -> rule7))]
("Bob" "is" "green" "-")
((triple5) -> (rule7 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Dave is quiet.
True
4
proof
[(((((triple7) -> rule7) triple9) -> rule4))]
("Dave" "is" "quiet" "+")
((((triple7) -> (rule7 % int2)) triple9) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Harry is not quiet.
False
5
inv-proof
[(((((triple11) -> rule7) ((triple10) -> rule8)) -> rule4))]
("Harry" "is" "quiet" "-")
((((triple11) -> (rule7 % int3)) ((triple10) -> (rule8 % int2))) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Bob is young.
True
5
proof
[(((((((triple5) -> rule7) triple5) -> rule1)) -> rule8))]
("Bob" "is" "young" "+")
((((((triple5) -> (rule7 % int3)) triple5) -> (rule1 % int2))) -> (rule8 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Harry is cold.
False
7
inv-proof
[(((triple10 ((((triple11) -> rule7) ((triple10) -> rule8)) -> rule4)) -> rule9))]
("Harry" "is" "cold" "+")
((triple10 ((((triple11) -> (rule7 % int4)) ((triple10) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule9 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
Bob is quiet.
True
8
proof
[(((((triple5) -> rule7) ((((((triple5) -> rule7) triple5) -> rule1)) -> rule8)) -> rule4))]
("Bob" "is" "quiet" "+")
((((triple5) -> (rule7 % int4)) ((((((triple5) -> (rule7 % int4)) triple5) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
Bob is not quiet.
False
8
inv-proof
[(((((triple5) -> rule7) ((((((triple5) -> rule7) triple5) -> rule1)) -> rule8)) -> rule4))]
("Bob" "is" "quiet" "-")
((((triple5) -> (rule7 % int4)) ((((((triple5) -> (rule7 % int4)) triple5) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
Bob is not cold.
True
13
proof
[(((((((triple5) -> rule7) triple5) -> rule1) ((((triple5) -> rule7) ((((((triple5) -> rule7) triple5) -> rule1)) -> rule8)) -> rule4)) -> rule9))]
("Bob" "is" "cold" "-")
((((((triple5) -> (rule7 % int5)) triple5) -> (rule1 % int4)) ((((triple5) -> (rule7 % int5)) ((((((triple5) -> (rule7 % int5)) triple5) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule9 % int1))
Bob is not cold.
("Bob" "is" "cold" "-")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
int4
Bob is green.
("Bob" "is" "green" "+")
int5
Bob is cold.
False
13
inv-proof
[(((((((triple5) -> rule7) triple5) -> rule1) ((((triple5) -> rule7) ((((((triple5) -> rule7) triple5) -> rule1)) -> rule8)) -> rule4)) -> rule9))]
("Bob" "is" "cold" "+")
((((((triple5) -> (rule7 % int5)) triple5) -> (rule1 % int4)) ((((triple5) -> (rule7 % int5)) ((((((triple5) -> (rule7 % int5)) triple5) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule9 % int1))
Bob is not cold.
("Bob" "is" "cold" "-")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
int4
Bob is green.
("Bob" "is" "green" "+")
int5
Anne is not green.
Unknown
inv-rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "green" "-")
Harry is smart.
Unknown
rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "smart" "+")
Anne is not young.
Unknown
inv-rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Anne" "is" "young" "-")
Bob is smart.
Unknown
rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "smart" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
@0: Anne is cold.[(triple1)] Anne is not furry.[(triple2)] Anne is not smart.[(triple4)] Anne is quiet.[(triple3)] Bob is round.[(triple5)] Dave is cold.[(triple6)] Dave is round.[(triple7)] Dave is smart.[(triple8 OR ((triple6 triple7) -> rule2))] Dave is young.[(triple9)] Harry is furry.[(triple10)] Harry is round.[(triple11)] @1: Bob is green.[(((triple5) -> rule7))] Dave is green.[(((triple7) -> rule7))] Harry is green.[(((triple11) -> rule7))] Harry is young.[(((triple10) -> rule8))] @2: Bob is furry.[(((((triple5) -> rule7) triple5) -> rule1))] Dave is quiet.[(((((triple7) -> rule7) triple9) -> rule4))] Harry is quiet.[(((((triple11) -> rule7) ((triple10) -> rule8)) -> rule4))] @3: Bob is young.[(((((((triple5) -> rule7) triple5) -> rule1)) -> rule8))] Harry is not cold.[(((triple10 ((((triple11) -> rule7) ((triple10) -> rule8)) -> rule4)) -> rule9))] @4: Bob is quiet.[(((((triple5) -> rule7) ((((((triple5) -> rule7) triple5) -> rule1)) -> rule8)) -> rule4))] @5: Bob is not cold.[(((((((triple5) -> rule7) triple5) -> rule1) ((((triple5) -> rule7) ((((((triple5) -> rule7) triple5) -> rule1)) -> rule8)) -> rule4)) -> rule9))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is not furry.
("Anne" "is" "furry" "-")
triple2
Anne is not smart.
("Anne" "is" "smart" "-")
triple4
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
Bob is round.
("Bob" "is" "round" "+")
triple5
Dave is cold.
("Dave" "is" "cold" "+")
triple6
Dave is round.
("Dave" "is" "round" "+")
triple7
Dave is smart.
("Dave" "is" "smart" "+")
triple8
((triple6 triple7) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
triple9
Harry is furry.
("Harry" "is" "furry" "+")
triple10
Harry is round.
("Harry" "is" "round" "+")
triple11
Bob is green.
("Bob" "is" "green" "+")
((triple5) -> (rule7 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((triple7) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((triple11) -> (rule7 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple10) -> (rule8 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((((triple5) -> (rule7 % int2)) triple5) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
((((triple7) -> (rule7 % int2)) triple9) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
((((triple11) -> (rule7 % int3)) ((triple10) -> (rule8 % int2))) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
((((((triple5) -> (rule7 % int3)) triple5) -> (rule1 % int2))) -> (rule8 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Harry is not cold.
("Harry" "is" "cold" "-")
((triple10 ((((triple11) -> (rule7 % int4)) ((triple10) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule9 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
Bob is quiet.
("Bob" "is" "quiet" "+")
((((triple5) -> (rule7 % int4)) ((((((triple5) -> (rule7 % int4)) triple5) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
Bob is not cold.
("Bob" "is" "cold" "-")
((((((triple5) -> (rule7 % int5)) triple5) -> (rule1 % int4)) ((((triple5) -> (rule7 % int5)) ((((((triple5) -> (rule7 % int5)) triple5) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule9 % int1))
Bob is not cold.
("Bob" "is" "cold" "-")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
int4
Bob is green.
("Bob" "is" "green" "+")
int5