Bob is big. Bob is not rough. Bob is smart. Bob is white. Dave is not big. Dave is smart. Fiona is big. Fiona is green. Fiona is kind. Fiona is nice. Fiona is not smart. Fiona is white. All kind people are rough. If someone is big and not kind then they are nice. All green people are nice. If someone is white then they are green. All nice, big people are green. If Dave is nice and Dave is green then Dave is white. All smart people are white. If Bob is green and Bob is rough then Bob is not nice.
Bob is big.
("Bob" "is" "big" "+")
Bob is not rough.
("Bob" "is" "rough" "-")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is not big.
("Dave" "is" "big" "-")
Dave is smart.
("Dave" "is" "smart" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is not smart.
("Fiona" "is" "smart" "-")
Fiona is white.
("Fiona" "is" "white" "+")
All kind people are rough.
((("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
If someone is big and not kind then they are nice.
((("someone" "is" "big" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "nice" "+"))
All green people are nice.
((("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
If someone is white then they are green.
((("someone" "is" "white" "+")) -> ("someone" "is" "green" "+"))
All nice, big people are green.
((("someone" "is" "nice" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
If Dave is nice and Dave is green then Dave is white.
((("Dave" "is" "nice" "+") ("Dave" "is" "green" "+")) -> ("Dave" "is" "white" "+"))
All smart people are white.
((("someone" "is" "smart" "+")) -> ("someone" "is" "white" "+"))
If Bob is green and Bob is rough then Bob is not nice.
((("Bob" "is" "green" "+") ("Bob" "is" "rough" "+")) -> ("Bob" "is" "nice" "-"))
Dave is not big.
True
1
proof
[(triple5)]
("Dave" "is" "big" "-")
triple5
Bob is not white.
False
1
inv-proof
[(triple4 OR ((triple3) -> rule7))]
("Bob" "is" "white" "-")
triple4
((triple3) -> (rule7 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Dave is white.
True
2
proof
[(((triple6) -> rule7))]
("Dave" "is" "white" "+")
((triple6) -> (rule7 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Bob is not green.
False
2
inv-proof
[(((triple4) -> rule4) OR ((((triple3) -> rule7)) -> rule4))]
("Bob" "is" "green" "-")
((triple4) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((((triple3) -> (rule7 % int2))) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is nice.
True
3
proof
[(((((triple4) -> rule4)) -> rule3) OR ((((((triple3) -> rule7)) -> rule4)) -> rule3))]
("Bob" "is" "nice" "+")
((((triple4) -> (rule4 % int2))) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((((((triple3) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is not nice.
False
3
inv-proof
[(((((triple4) -> rule4)) -> rule3) OR ((((((triple3) -> rule7)) -> rule4)) -> rule3))]
("Bob" "is" "nice" "-")
((((triple4) -> (rule4 % int2))) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((((((triple3) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Dave is nice.
True
4
proof
[(((((((triple6) -> rule7)) -> rule4)) -> rule3))]
("Dave" "is" "nice" "+")
((((((triple6) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is not nice.
False
4
inv-proof
[(((((((triple6) -> rule7)) -> rule4)) -> rule3))]
("Dave" "is" "nice" "-")
((((((triple6) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is not rough.
Unknown
inv-rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "rough" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
@0: Bob is big.[(triple1)] Bob is not rough.[(triple2)] Bob is smart.[(triple3)] Bob is white.[(triple4 OR ((triple3) -> rule7))] Dave is not big.[(triple5)] Dave is smart.[(triple6)] Fiona is big.[(triple7)] Fiona is green.[(triple8 OR ((triple12) -> rule4) OR ((triple10 triple7) -> rule5))] Fiona is kind.[(triple9)] Fiona is nice.[(triple10 OR ((triple8) -> rule3) OR ((((triple12) -> rule4)) -> rule3))] Fiona is not smart.[(triple11)] Fiona is white.[(triple12)] @1: Bob is green.[(((triple4) -> rule4) OR ((((triple3) -> rule7)) -> rule4))] Dave is white.[(((triple6) -> rule7))] Fiona is rough.[(((triple9) -> rule1))] @2: Bob is nice.[(((((triple4) -> rule4)) -> rule3) OR ((((((triple3) -> rule7)) -> rule4)) -> rule3))] Dave is green.[(((((triple6) -> rule7)) -> rule4))] @3: Dave is nice.[(((((((triple6) -> rule7)) -> rule4)) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is not rough.
("Bob" "is" "rough" "-")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Bob is white.
("Bob" "is" "white" "+")
triple4
((triple3) -> (rule7 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Dave is not big.
("Dave" "is" "big" "-")
triple5
Dave is smart.
("Dave" "is" "smart" "+")
triple6
Fiona is big.
("Fiona" "is" "big" "+")
triple7
Fiona is green.
("Fiona" "is" "green" "+")
triple8
((triple12) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((triple10 triple7) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
triple9
Fiona is nice.
("Fiona" "is" "nice" "+")
triple10
((triple8) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
((((triple12) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is not smart.
("Fiona" "is" "smart" "-")
triple11
Fiona is white.
("Fiona" "is" "white" "+")
triple12
Bob is green.
("Bob" "is" "green" "+")
((triple4) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((((triple3) -> (rule7 % int2))) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
((triple6) -> (rule7 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple9) -> (rule1 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((((triple4) -> (rule4 % int2))) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((((((triple3) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
((((triple6) -> (rule7 % int2))) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
((((((triple6) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3