Bob is nice. Bob is white. Charlie is quiet. Charlie is red. Dave is kind. Dave is nice. Dave is quiet. Dave is red. Dave is rough. Fiona is nice. Fiona is rough. Fiona is smart. All red, white things are quiet. Kind things are smart. If Charlie is nice then Charlie is white. If Fiona is kind then Fiona is nice. If something is white then it is rough. If something is smart then it is nice. All red things are nice. Rough things are kind.
Bob is nice.
("Bob" "is" "nice" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
All red, white things are quiet.
((("something" "is" "red" "+") ("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
Kind things are smart.
((("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
If Charlie is nice then Charlie is white.
((("Charlie" "is" "nice" "+")) -> ("Charlie" "is" "white" "+"))
If Fiona is kind then Fiona is nice.
((("Fiona" "is" "kind" "+")) -> ("Fiona" "is" "nice" "+"))
If something is white then it is rough.
((("something" "is" "white" "+")) -> ("something" "is" "rough" "+"))
If something is smart then it is nice.
((("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
All red things are nice.
((("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
Rough things are kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
Fiona is nice.
True
1
proof
[(triple10 OR ((triple12) -> rule6) OR ((((triple11) -> rule8)) -> rule4) OR ((((((triple11) -> rule8)) -> rule2)) -> rule6))]
("Fiona" "is" "nice" "+")
triple10
((triple12) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
((((triple11) -> (rule8 % int2))) -> (rule4 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
((((((triple11) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Dave is not nice.
False
1
inv-proof
[(triple6 OR ((triple8) -> rule7) OR ((((triple5) -> rule2)) -> rule6) OR ((((((triple9) -> rule8)) -> rule2)) -> rule6))]
("Dave" "is" "nice" "-")
triple6
((triple8) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((((triple5) -> (rule2 % int2))) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((((((triple9) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Charlie is nice.
True
2
proof
[(((triple4) -> rule7))]
("Charlie" "is" "nice" "+")
((triple4) -> (rule7 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Bob is not rough.
False
2
inv-proof
[(((triple2) -> rule5))]
("Bob" "is" "rough" "-")
((triple2) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is kind.
True
3
proof
[(((((triple2) -> rule5)) -> rule8))]
("Bob" "is" "kind" "+")
((((triple2) -> (rule5 % int2))) -> (rule8 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Charlie is not white.
False
3
inv-proof
[(((((triple4) -> rule7)) -> rule3))]
("Charlie" "is" "white" "-")
((((triple4) -> (rule7 % int2))) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Bob is smart.
True
4
proof
[(((((((triple2) -> rule5)) -> rule8)) -> rule2))]
("Bob" "is" "smart" "+")
((((((triple2) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Charlie is not rough.
False
4
inv-proof
[(((((((triple4) -> rule7)) -> rule3)) -> rule5))]
("Charlie" "is" "rough" "-")
((((((triple4) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is kind.
True
5
proof
[(((((((((triple4) -> rule7)) -> rule3)) -> rule5)) -> rule8))]
("Charlie" "is" "kind" "+")
((((((((triple4) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
Charlie is not kind.
False
5
inv-proof
[(((((((((triple4) -> rule7)) -> rule3)) -> rule5)) -> rule8))]
("Charlie" "is" "kind" "-")
((((((((triple4) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
Charlie is smart.
True
6
proof
[(((((((((((triple4) -> rule7)) -> rule3)) -> rule5)) -> rule8)) -> rule2))]
("Charlie" "is" "smart" "+")
((((((((((triple4) -> (rule7 % int5))) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
Charlie is nice.
("Charlie" "is" "nice" "+")
int5
Charlie is not smart.
False
6
inv-proof
[(((((((((((triple4) -> rule7)) -> rule3)) -> rule5)) -> rule8)) -> rule2))]
("Charlie" "is" "smart" "-")
((((((((((triple4) -> (rule7 % int5))) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
Charlie is nice.
("Charlie" "is" "nice" "+")
int5
Bob is not quiet.
Unknown
inv-rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "quiet" "-")
Fiona is quiet.
Unknown
rconc
[@1: Fiona is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "quiet" "+")
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Fiona is white.
Unknown
random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "+")
Bob is not red.
Unknown
inv-random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "-")
Fiona is red.
Unknown
random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "+")
@0: Bob is nice.[(triple1 OR ((((((((triple2) -> rule5)) -> rule8)) -> rule2)) -> rule6))] Bob is white.[(triple2)] Charlie is quiet.[(triple3 OR ((triple4 ((((triple4) -> rule7)) -> rule3)) -> rule1))] Charlie is red.[(triple4)] Dave is kind.[(triple5 OR ((triple9) -> rule8))] Dave is nice.[(triple6 OR ((triple8) -> rule7) OR ((((triple5) -> rule2)) -> rule6) OR ((((((triple9) -> rule8)) -> rule2)) -> rule6))] Dave is quiet.[(triple7)] Dave is red.[(triple8)] Dave is rough.[(triple9)] Fiona is nice.[(triple10 OR ((triple12) -> rule6) OR ((((triple11) -> rule8)) -> rule4) OR ((((((triple11) -> rule8)) -> rule2)) -> rule6))] Fiona is rough.[(triple11)] Fiona is smart.[(triple12 OR ((((triple11) -> rule8)) -> rule2))] @1: Bob is rough.[(((triple2) -> rule5))] Charlie is nice.[(((triple4) -> rule7))] Dave is smart.[(((triple5) -> rule2) OR ((((triple9) -> rule8)) -> rule2))] Fiona is kind.[(((triple11) -> rule8))] @2: Bob is kind.[(((((triple2) -> rule5)) -> rule8))] Charlie is white.[(((((triple4) -> rule7)) -> rule3))] @3: Bob is smart.[(((((((triple2) -> rule5)) -> rule8)) -> rule2))] Charlie is rough.[(((((((triple4) -> rule7)) -> rule3)) -> rule5))] @4: Charlie is kind.[(((((((((triple4) -> rule7)) -> rule3)) -> rule5)) -> rule8))] @5: Charlie is smart.[(((((((((((triple4) -> rule7)) -> rule3)) -> rule5)) -> rule8)) -> rule2))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
((((((((triple2) -> (rule5 % int4))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
int4
Bob is white.
("Bob" "is" "white" "+")
triple2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
((triple4 ((((triple4) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
triple4
Dave is kind.
("Dave" "is" "kind" "+")
triple5
((triple9) -> (rule8 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
triple6
((triple8) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((((triple5) -> (rule2 % int2))) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((((((triple9) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
triple7
Dave is red.
("Dave" "is" "red" "+")
triple8
Dave is rough.
("Dave" "is" "rough" "+")
triple9
Fiona is nice.
("Fiona" "is" "nice" "+")
triple10
((triple12) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
((((triple11) -> (rule8 % int2))) -> (rule4 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
((((((triple11) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
triple11
Fiona is smart.
("Fiona" "is" "smart" "+")
triple12
((((triple11) -> (rule8 % int2))) -> (rule2 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
((triple2) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple4) -> (rule7 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple5) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((((triple9) -> (rule8 % int2))) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple11) -> (rule8 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((((triple2) -> (rule5 % int2))) -> (rule8 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
((((triple4) -> (rule7 % int2))) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
((((((triple2) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
((((((triple4) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
((((((((triple4) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
Charlie is smart.
("Charlie" "is" "smart" "+")
((((((((((triple4) -> (rule7 % int5))) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
Charlie is nice.
("Charlie" "is" "nice" "+")
int5