Bob is quiet. Erin is not quiet. Erin is red. Erin is rough. Fiona is nice. Fiona is quiet. Fiona is red. Fiona is not round. Fiona is smart. Harry is furry. If someone is quiet then they are rough. All smart, red people are not round. All smart, rough people are red. All rough people are smart. All round people are nice. If someone is quiet and not nice then they are furry.
Bob is quiet.
("Bob" "is" "quiet" "+")
Erin is not quiet.
("Erin" "is" "quiet" "-")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is not round.
("Fiona" "is" "round" "-")
Fiona is smart.
("Fiona" "is" "smart" "+")
Harry is furry.
("Harry" "is" "furry" "+")
If someone is quiet then they are rough.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
All smart, red people are not round.
((("someone" "is" "smart" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "round" "-"))
All smart, rough people are red.
((("someone" "is" "smart" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
All rough people are smart.
((("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
All round people are nice.
((("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
If someone is quiet and not nice then they are furry.
((("someone" "is" "quiet" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "furry" "+"))
Fiona is not round.
True
1
proof
[(triple8 OR ((triple9 triple7) -> rule2) OR ((triple9 ((triple9 ((triple6) -> rule1)) -> rule3)) -> rule2) OR ((((((triple6) -> rule1)) -> rule4) triple7) -> rule2) OR ((((((triple6) -> rule1)) -> rule4) ((triple9 ((triple6) -> rule1)) -> rule3)) -> rule2) OR ((triple9 ((((((triple6) -> rule1)) -> rule4) ((triple6) -> rule1)) -> rule3)) -> rule2) OR ((((((triple6) -> rule1)) -> rule4) ((((((triple6) -> rule1)) -> rule4) ((triple6) -> rule1)) -> rule3)) -> rule2))]
("Fiona" "is" "round" "-")
triple8
((triple9 triple7) -> (rule2 % int1))
Fiona is not round.
("Fiona" "is" "round" "-")
int1
((triple9 ((triple9 ((triple6) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is not round.
("Fiona" "is" "round" "-")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
((((((triple6) -> (rule1 % int3))) -> (rule4 % int2)) triple7) -> (rule2 % int1))
Fiona is not round.
("Fiona" "is" "round" "-")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
((((((triple6) -> (rule1 % int4))) -> (rule4 % int3)) ((triple9 ((triple6) -> (rule1 % int4))) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is not round.
("Fiona" "is" "round" "-")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
int4
((triple9 ((((((triple6) -> (rule1 % int4))) -> (rule4 % int3)) ((triple6) -> (rule1 % int4))) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is not round.
("Fiona" "is" "round" "-")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
int4
((((((triple6) -> (rule1 % int4))) -> (rule4 % int3)) ((((((triple6) -> (rule1 % int4))) -> (rule4 % int3)) ((triple6) -> (rule1 % int4))) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is not round.
("Fiona" "is" "round" "-")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
int4
Erin is quiet.
False
1
inv-proof
[(triple2)]
("Erin" "is" "quiet" "+")
triple2
Bob is rough.
True
2
proof
[(((triple1) -> rule1))]
("Bob" "is" "rough" "+")
((triple1) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is not rough.
False
2
inv-proof
[(((triple1) -> rule1))]
("Bob" "is" "rough" "-")
((triple1) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is smart.
True
3
proof
[(((((triple1) -> rule1)) -> rule4))]
("Bob" "is" "smart" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Erin is round.
False
4
inv-proof
[(((((triple4) -> rule4) triple3) -> rule2) OR ((((triple4) -> rule4) ((((triple4) -> rule4) triple4) -> rule3)) -> rule2))]
("Erin" "is" "round" "+")
((((triple4) -> (rule4 % int2)) triple3) -> (rule2 % int1))
Erin is not round.
("Erin" "is" "round" "-")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((triple4) -> (rule4 % int3)) ((((triple4) -> (rule4 % int3)) triple4) -> (rule3 % int2))) -> (rule2 % int1))
Erin is not round.
("Erin" "is" "round" "-")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Bob is red.
True
6
proof
[(((((((triple1) -> rule1)) -> rule4) ((triple1) -> rule1)) -> rule3))]
("Bob" "is" "red" "+")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2)) ((triple1) -> (rule1 % int3))) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is not red.
False
6
inv-proof
[(((((((triple1) -> rule1)) -> rule4) ((triple1) -> rule1)) -> rule3))]
("Bob" "is" "red" "-")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2)) ((triple1) -> (rule1 % int3))) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Fiona is not furry.
Unknown
inv-rconc
[@1: Fiona is furry.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "furry" "-")
Harry is red.
Unknown
rconc
[@2: Harry is red.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Harry" "is" "red" "+")
Bob is not nice.
Unknown
inv-rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "nice" "-")
Erin is nice.
Unknown
rconc
[@1: Erin is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "nice" "+")
Harry is not quiet.
Unknown
inv-random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
@0: Bob is quiet.[(triple1)] Erin is not quiet.[(triple2)] Erin is red.[(triple3 OR ((((triple4) -> rule4) triple4) -> rule3))] Erin is rough.[(triple4)] Fiona is nice.[(triple5)] Fiona is not round.[(triple8 OR ((triple9 triple7) -> rule2) OR ((triple9 ((triple9 ((triple6) -> rule1)) -> rule3)) -> rule2) OR ((((((triple6) -> rule1)) -> rule4) triple7) -> rule2) OR ((((((triple6) -> rule1)) -> rule4) ((triple9 ((triple6) -> rule1)) -> rule3)) -> rule2) OR ((triple9 ((((((triple6) -> rule1)) -> rule4) ((triple6) -> rule1)) -> rule3)) -> rule2) OR ((((((triple6) -> rule1)) -> rule4) ((((((triple6) -> rule1)) -> rule4) ((triple6) -> rule1)) -> rule3)) -> rule2))] Fiona is quiet.[(triple6)] Fiona is red.[(triple7 OR ((triple9 ((triple6) -> rule1)) -> rule3) OR ((((((triple6) -> rule1)) -> rule4) ((triple6) -> rule1)) -> rule3))] Fiona is smart.[(triple9 OR ((((triple6) -> rule1)) -> rule4))] Harry is furry.[(triple10)] @1: Bob is rough.[(((triple1) -> rule1))] Erin is smart.[(((triple4) -> rule4))] Fiona is rough.[(((triple6) -> rule1))] @2: Bob is smart.[(((((triple1) -> rule1)) -> rule4))] Erin is not round.[(((((triple4) -> rule4) triple3) -> rule2) OR ((((triple4) -> rule4) ((((triple4) -> rule4) triple4) -> rule3)) -> rule2))] @3: Bob is red.[(((((((triple1) -> rule1)) -> rule4) ((triple1) -> rule1)) -> rule3))] @4: Bob is not round.[(((((((triple1) -> rule1)) -> rule4) ((((((triple1) -> rule1)) -> rule4) ((triple1) -> rule1)) -> rule3)) -> rule2))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Erin is not quiet.
("Erin" "is" "quiet" "-")
triple2
Erin is red.
("Erin" "is" "red" "+")
triple3
((((triple4) -> (rule4 % int2)) triple4) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
triple4
Fiona is nice.
("Fiona" "is" "nice" "+")
triple5
Fiona is not round.
("Fiona" "is" "round" "-")
triple8
((triple9 triple7) -> (rule2 % int1))
Fiona is not round.
("Fiona" "is" "round" "-")
int1
((triple9 ((triple9 ((triple6) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is not round.
("Fiona" "is" "round" "-")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
((((((triple6) -> (rule1 % int3))) -> (rule4 % int2)) triple7) -> (rule2 % int1))
Fiona is not round.
("Fiona" "is" "round" "-")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
((((((triple6) -> (rule1 % int4))) -> (rule4 % int3)) ((triple9 ((triple6) -> (rule1 % int4))) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is not round.
("Fiona" "is" "round" "-")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
int4
((triple9 ((((((triple6) -> (rule1 % int4))) -> (rule4 % int3)) ((triple6) -> (rule1 % int4))) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is not round.
("Fiona" "is" "round" "-")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
int4
((((((triple6) -> (rule1 % int4))) -> (rule4 % int3)) ((((((triple6) -> (rule1 % int4))) -> (rule4 % int3)) ((triple6) -> (rule1 % int4))) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is not round.
("Fiona" "is" "round" "-")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
int4
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple6
Fiona is red.
("Fiona" "is" "red" "+")
triple7
((triple9 ((triple6) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
((((((triple6) -> (rule1 % int3))) -> (rule4 % int2)) ((triple6) -> (rule1 % int3))) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
triple9
((((triple6) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
triple10
Bob is rough.
("Bob" "is" "rough" "+")
((triple1) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple4) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple6) -> (rule1 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Erin is not round.
("Erin" "is" "round" "-")
((((triple4) -> (rule4 % int2)) triple3) -> (rule2 % int1))
Erin is not round.
("Erin" "is" "round" "-")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((triple4) -> (rule4 % int3)) ((((triple4) -> (rule4 % int3)) triple4) -> (rule3 % int2))) -> (rule2 % int1))
Erin is not round.
("Erin" "is" "round" "-")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2)) ((triple1) -> (rule1 % int3))) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is not round.
("Bob" "is" "round" "-")
((((((triple1) -> (rule1 % int4))) -> (rule4 % int3)) ((((((triple1) -> (rule1 % int4))) -> (rule4 % int3)) ((triple1) -> (rule1 % int4))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is not round.
("Bob" "is" "round" "-")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
int4