Anne is round. Bob is blue. Bob is round. Bob is smart. Dave is nice. Dave is round. Dave is smart. Dave is white. Dave is young. Fiona is smart. If something is smart then it is white. If something is white then it is not rough. White things are blue. If Fiona is not white then Fiona is nice. All blue things are young. If something is white and not blue then it is young. If something is white then it is nice. All young, smart things are nice.
Anne is round.
("Anne" "is" "round" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
If something is smart then it is white.
((("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
If something is white then it is not rough.
((("something" "is" "white" "+")) -> ("something" "is" "rough" "-"))
White things are blue.
((("something" "is" "white" "+")) -> ("something" "is" "blue" "+"))
If Fiona is not white then Fiona is nice.
((("Fiona" "is" "white" "~")) -> ("Fiona" "is" "nice" "+"))
All blue things are young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
If something is white and not blue then it is young.
((("something" "is" "white" "+") ("something" "is" "blue" "~")) -> ("something" "is" "young" "+"))
If something is white then it is nice.
((("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
All young, smart things are nice.
((("something" "is" "young" "+") ("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
Dave is white.
True
1
proof
[(triple8 OR ((triple7) -> rule1))]
("Dave" "is" "white" "+")
triple8
((triple7) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is not smart.
False
1
inv-proof
[(triple7)]
("Dave" "is" "smart" "-")
triple7
Bob is young.
True
2
proof
[(((triple2) -> rule5) OR ((((((triple4) -> rule1)) -> rule3)) -> rule5))]
("Bob" "is" "young" "+")
((triple2) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((((((triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is not white.
False
2
inv-proof
[(((triple4) -> rule1))]
("Bob" "is" "white" "-")
((triple4) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Fiona is blue.
True
3
proof
[(((((triple10) -> rule1)) -> rule3))]
("Fiona" "is" "blue" "+")
((((triple10) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is rough.
False
3
inv-proof
[(((((triple10) -> rule1)) -> rule2))]
("Fiona" "is" "rough" "+")
((((triple10) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is not rough.
("Fiona" "is" "rough" "-")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is young.
True
4
proof
[(((((((triple10) -> rule1)) -> rule3)) -> rule5))]
("Fiona" "is" "young" "+")
((((((triple10) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Fiona is not young.
False
4
inv-proof
[(((((((triple10) -> rule1)) -> rule3)) -> rule5))]
("Fiona" "is" "young" "-")
((((((triple10) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Anne is not blue.
Unknown
inv-rconc
[@2: Anne is blue.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Anne" "is" "blue" "-")
Anne is nice.
Unknown
rconc
[@2: Anne is nice.[CWA. Example of deepest failure = (rule7 <- rule1 <- FAIL)]]
("Anne" "is" "nice" "+")
Anne is not young.
Unknown
inv-rconc
[@3: Anne is young.[CWA. Example of deepest failure = (rule5 <- rule3 <- rule1 <- FAIL)]]
("Anne" "is" "young" "-")
Anne is white.
Unknown
rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "white" "+")
Anne is not smart.
Unknown
inv-random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
@0: Anne is round.[(triple1)] Bob is blue.[(triple2 OR ((((triple4) -> rule1)) -> rule3))] Bob is round.[(triple3)] Bob is smart.[(triple4)] Dave is nice.[(triple5 OR ((triple8) -> rule7) OR ((triple9 triple7) -> rule8) OR ((((triple7) -> rule1)) -> rule7) OR ((((((triple8) -> rule3)) -> rule5) triple7) -> rule8) OR ((((((((triple7) -> rule1)) -> rule3)) -> rule5) triple7) -> rule8))] Dave is round.[(triple6)] Dave is smart.[(triple7)] Dave is white.[(triple8 OR ((triple7) -> rule1))] Dave is young.[(triple9 OR ((((triple8) -> rule3)) -> rule5) OR ((((((triple7) -> rule1)) -> rule3)) -> rule5))] Fiona is smart.[(triple10)] @1: Bob is white.[(((triple4) -> rule1))] Bob is young.[(((triple2) -> rule5) OR ((((((triple4) -> rule1)) -> rule3)) -> rule5))] Dave is blue.[(((triple8) -> rule3) OR ((((triple7) -> rule1)) -> rule3))] Dave is not rough.[(((triple8) -> rule2) OR ((((triple7) -> rule1)) -> rule2))] Fiona is white.[(((triple10) -> rule1))] @2: Bob is nice.[(((((triple4) -> rule1)) -> rule7) OR ((((triple2) -> rule5) triple4) -> rule8) OR ((((((((triple4) -> rule1)) -> rule3)) -> rule5) triple4) -> rule8))] Bob is not rough.[(((((triple4) -> rule1)) -> rule2))] Fiona is blue.[(((((triple10) -> rule1)) -> rule3))] Fiona is nice.[(((((triple10) -> rule1)) -> rule7) OR ((((((((triple10) -> rule1)) -> rule3)) -> rule5) triple10) -> rule8))] Fiona is not rough.[(((((triple10) -> rule1)) -> rule2))] @3: Fiona is young.[(((((((triple10) -> rule1)) -> rule3)) -> rule5))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
triple4
Dave is nice.
("Dave" "is" "nice" "+")
triple5
((triple8) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple9 triple7) -> (rule8 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((((triple7) -> (rule1 % int2))) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((((triple8) -> (rule3 % int3))) -> (rule5 % int2)) triple7) -> (rule8 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
((((((((triple7) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule5 % int2)) triple7) -> (rule8 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Dave is round.
("Dave" "is" "round" "+")
triple6
Dave is smart.
("Dave" "is" "smart" "+")
triple7
Dave is white.
("Dave" "is" "white" "+")
triple8
((triple7) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
triple9
((((triple8) -> (rule3 % int2))) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
((((((triple7) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
triple10
Bob is white.
("Bob" "is" "white" "+")
((triple4) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
((triple2) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((((((triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
((triple8) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple7) -> (rule1 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is not rough.
("Dave" "is" "rough" "-")
((triple8) -> (rule2 % int1))
Dave is not rough.
("Dave" "is" "rough" "-")
int1
((((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Dave is not rough.
("Dave" "is" "rough" "-")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
((triple10) -> (rule1 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((((triple4) -> (rule1 % int2))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
((((triple2) -> (rule5 % int2)) triple4) -> (rule8 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
((((((((triple4) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule5 % int2)) triple4) -> (rule8 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Bob is not rough.
("Bob" "is" "rough" "-")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Bob is not rough.
("Bob" "is" "rough" "-")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
((((triple10) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
((((triple10) -> (rule1 % int2))) -> (rule7 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
((((((((triple10) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule5 % int2)) triple10) -> (rule8 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
int4
Fiona is not rough.
("Fiona" "is" "rough" "-")
((((triple10) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is not rough.
("Fiona" "is" "rough" "-")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
((((((triple10) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3