Bob is furry. Bob is round. Bob is smart. Dave is cold. Dave is round. Dave is smart. Dave is young. Fiona is big. Fiona is young. Gary is round. If Dave is round then Dave is quiet. Big, young people are round. All quiet, big people are smart. All round, young people are quiet. Young people are big. All cold, round people are quiet.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is round.
("Gary" "is" "round" "+")
If Dave is round then Dave is quiet.
((("Dave" "is" "round" "+")) -> ("Dave" "is" "quiet" "+"))
Big, young people are round.
((("someone" "is" "big" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
All quiet, big people are smart.
((("someone" "is" "quiet" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
All round, young people are quiet.
((("someone" "is" "round" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "+"))
Young people are big.
((("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
All cold, round people are quiet.
((("someone" "is" "cold" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
Bob is round.
True
1
proof
[(triple2)]
("Bob" "is" "round" "+")
triple2
Fiona is not big.
False
1
inv-proof
[(triple8 OR ((triple9) -> rule5))]
("Fiona" "is" "big" "-")
triple8
((triple9) -> (rule5 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Dave is quiet.
True
2
proof
[(((triple5) -> rule1) OR ((triple4 triple5) -> rule6) OR ((triple5 triple7) -> rule4) OR ((((((triple7) -> rule5) triple7) -> rule2)) -> rule1) OR ((triple4 ((((triple7) -> rule5) triple7) -> rule2)) -> rule6) OR ((((((triple7) -> rule5) triple7) -> rule2) triple7) -> rule4))]
("Dave" "is" "quiet" "+")
((triple5) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((triple4 triple5) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((triple5 triple7) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((((((triple7) -> (rule5 % int3)) triple7) -> (rule2 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
((triple4 ((((triple7) -> (rule5 % int3)) triple7) -> (rule2 % int2))) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
((((((triple7) -> (rule5 % int3)) triple7) -> (rule2 % int2)) triple7) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Fiona is not round.
False
3
inv-proof
[(((triple8 triple9) -> rule2) OR ((((triple9) -> rule5) triple9) -> rule2))]
("Fiona" "is" "round" "-")
((triple8 triple9) -> (rule2 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
((((triple9) -> (rule5 % int2)) triple9) -> (rule2 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is quiet.
True
5
proof
[(((((triple8 triple9) -> rule2) triple9) -> rule4) OR ((((((triple9) -> rule5) triple9) -> rule2) triple9) -> rule4))]
("Fiona" "is" "quiet" "+")
((((triple8 triple9) -> (rule2 % int2)) triple9) -> (rule4 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
((((((triple9) -> (rule5 % int3)) triple9) -> (rule2 % int2)) triple9) -> (rule4 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is not quiet.
False
5
inv-proof
[(((((triple8 triple9) -> rule2) triple9) -> rule4) OR ((((((triple9) -> rule5) triple9) -> rule2) triple9) -> rule4))]
("Fiona" "is" "quiet" "-")
((((triple8 triple9) -> (rule2 % int2)) triple9) -> (rule4 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
((((((triple9) -> (rule5 % int3)) triple9) -> (rule2 % int2)) triple9) -> (rule4 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is smart.
True
7
proof
[(((((((triple8 triple9) -> rule2) triple9) -> rule4) triple8) -> rule3) OR ((((((triple8 triple9) -> rule2) triple9) -> rule4) ((triple9) -> rule5)) -> rule3) OR ((((((((triple9) -> rule5) triple9) -> rule2) triple9) -> rule4) triple8) -> rule3) OR ((((((((triple9) -> rule5) triple9) -> rule2) triple9) -> rule4) ((triple9) -> rule5)) -> rule3))]
("Fiona" "is" "smart" "+")
((((((triple8 triple9) -> (rule2 % int3)) triple9) -> (rule4 % int2)) triple8) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
((((((triple8 triple9) -> (rule2 % int4)) triple9) -> (rule4 % int3)) ((triple9) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
int4
((((((((triple9) -> (rule5 % int4)) triple9) -> (rule2 % int3)) triple9) -> (rule4 % int2)) triple8) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is big.
("Fiona" "is" "big" "+")
int4
((((((((triple9) -> (rule5 % int4)) triple9) -> (rule2 % int3)) triple9) -> (rule4 % int2)) ((triple9) -> (rule5 % int4))) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is big.
("Fiona" "is" "big" "+")
int4
Fiona is not smart.
False
7
inv-proof
[(((((((triple8 triple9) -> rule2) triple9) -> rule4) triple8) -> rule3) OR ((((((triple8 triple9) -> rule2) triple9) -> rule4) ((triple9) -> rule5)) -> rule3) OR ((((((((triple9) -> rule5) triple9) -> rule2) triple9) -> rule4) triple8) -> rule3) OR ((((((((triple9) -> rule5) triple9) -> rule2) triple9) -> rule4) ((triple9) -> rule5)) -> rule3))]
("Fiona" "is" "smart" "-")
((((((triple8 triple9) -> (rule2 % int3)) triple9) -> (rule4 % int2)) triple8) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
((((((triple8 triple9) -> (rule2 % int4)) triple9) -> (rule4 % int3)) ((triple9) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
int4
((((((((triple9) -> (rule5 % int4)) triple9) -> (rule2 % int3)) triple9) -> (rule4 % int2)) triple8) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is big.
("Fiona" "is" "big" "+")
int4
((((((((triple9) -> (rule5 % int4)) triple9) -> (rule2 % int3)) triple9) -> (rule4 % int2)) ((triple9) -> (rule5 % int4))) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is big.
("Fiona" "is" "big" "+")
int4
Gary is not quiet.
Unknown
inv-rconc
[@1: Gary is quiet.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "quiet" "-")
Gary is smart.
Unknown
rconc
[@2: Gary is smart.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("Gary" "is" "smart" "+")
Bob is not big.
Unknown
inv-rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "big" "-")
Gary is big.
Unknown
rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "big" "+")
Gary is not cold.
Unknown
inv-random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
Bob is not young.
Unknown
inv-random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
@0: Bob is furry.[(triple1)] Bob is round.[(triple2)] Bob is smart.[(triple3)] Dave is cold.[(triple4)] Dave is round.[(triple5 OR ((((triple7) -> rule5) triple7) -> rule2))] Dave is smart.[(triple6 OR ((((triple5) -> rule1) ((triple7) -> rule5)) -> rule3) OR ((((triple4 triple5) -> rule6) ((triple7) -> rule5)) -> rule3) OR ((((triple5 triple7) -> rule4) ((triple7) -> rule5)) -> rule3) OR ((((((((triple7) -> rule5) triple7) -> rule2)) -> rule1) ((triple7) -> rule5)) -> rule3) OR ((((triple4 ((((triple7) -> rule5) triple7) -> rule2)) -> rule6) ((triple7) -> rule5)) -> rule3) OR ((((((((triple7) -> rule5) triple7) -> rule2) triple7) -> rule4) ((triple7) -> rule5)) -> rule3))] Dave is young.[(triple7)] Fiona is big.[(triple8 OR ((triple9) -> rule5))] Fiona is young.[(triple9)] Gary is round.[(triple10)] @1: Dave is big.[(((triple7) -> rule5))] Dave is quiet.[(((triple5) -> rule1) OR ((triple4 triple5) -> rule6) OR ((triple5 triple7) -> rule4) OR ((((((triple7) -> rule5) triple7) -> rule2)) -> rule1) OR ((triple4 ((((triple7) -> rule5) triple7) -> rule2)) -> rule6) OR ((((((triple7) -> rule5) triple7) -> rule2) triple7) -> rule4))] Fiona is round.[(((triple8 triple9) -> rule2) OR ((((triple9) -> rule5) triple9) -> rule2))] @2: Fiona is quiet.[(((((triple8 triple9) -> rule2) triple9) -> rule4) OR ((((((triple9) -> rule5) triple9) -> rule2) triple9) -> rule4))] @3: Fiona is smart.[(((((((triple8 triple9) -> rule2) triple9) -> rule4) triple8) -> rule3) OR ((((((triple8 triple9) -> rule2) triple9) -> rule4) ((triple9) -> rule5)) -> rule3) OR ((((((((triple9) -> rule5) triple9) -> rule2) triple9) -> rule4) triple8) -> rule3) OR ((((((((triple9) -> rule5) triple9) -> rule2) triple9) -> rule4) ((triple9) -> rule5)) -> rule3))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Dave is cold.
("Dave" "is" "cold" "+")
triple4
Dave is round.
("Dave" "is" "round" "+")
triple5
((((triple7) -> (rule5 % int2)) triple7) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
triple6
((((triple5) -> (rule1 % int3)) ((triple7) -> (rule5 % int2))) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
((((triple4 triple5) -> (rule6 % int3)) ((triple7) -> (rule5 % int2))) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
((((triple5 triple7) -> (rule4 % int3)) ((triple7) -> (rule5 % int2))) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
((((((((triple7) -> (rule5 % int4)) triple7) -> (rule2 % int3))) -> (rule1 % int2)) ((triple7) -> (rule5 % int4))) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
((((triple4 ((((triple7) -> (rule5 % int4)) triple7) -> (rule2 % int3))) -> (rule6 % int2)) ((triple7) -> (rule5 % int4))) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
((((((((triple7) -> (rule5 % int4)) triple7) -> (rule2 % int3)) triple7) -> (rule4 % int2)) ((triple7) -> (rule5 % int4))) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
Dave is young.
("Dave" "is" "young" "+")
triple7
Fiona is big.
("Fiona" "is" "big" "+")
triple8
((triple9) -> (rule5 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
triple9
Gary is round.
("Gary" "is" "round" "+")
triple10
Dave is big.
("Dave" "is" "big" "+")
((triple7) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple5) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((triple4 triple5) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((triple5 triple7) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((((((triple7) -> (rule5 % int3)) triple7) -> (rule2 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
((triple4 ((((triple7) -> (rule5 % int3)) triple7) -> (rule2 % int2))) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
((((((triple7) -> (rule5 % int3)) triple7) -> (rule2 % int2)) triple7) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
((triple8 triple9) -> (rule2 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
((((triple9) -> (rule5 % int2)) triple9) -> (rule2 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((((triple8 triple9) -> (rule2 % int2)) triple9) -> (rule4 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
((((((triple9) -> (rule5 % int3)) triple9) -> (rule2 % int2)) triple9) -> (rule4 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
((((((triple8 triple9) -> (rule2 % int3)) triple9) -> (rule4 % int2)) triple8) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
((((((triple8 triple9) -> (rule2 % int4)) triple9) -> (rule4 % int3)) ((triple9) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
int4
((((((((triple9) -> (rule5 % int4)) triple9) -> (rule2 % int3)) triple9) -> (rule4 % int2)) triple8) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is big.
("Fiona" "is" "big" "+")
int4
((((((((triple9) -> (rule5 % int4)) triple9) -> (rule2 % int3)) triple9) -> (rule4 % int2)) ((triple9) -> (rule5 % int4))) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is big.
("Fiona" "is" "big" "+")
int4