Bob is big. Bob is not cold. Bob is nice. Bob is white. Dave is not nice. Dave is quiet. Dave is not red. Dave is smart. Dave is not white. Fiona is quiet. Fiona is not red. Fiona is smart. If someone is smart and not white then they are not big.
Bob is big.
("Bob" "is" "big" "+")
Bob is not cold.
("Bob" "is" "cold" "-")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is not nice.
("Dave" "is" "nice" "-")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is not red.
("Dave" "is" "red" "-")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is not white.
("Dave" "is" "white" "-")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is not red.
("Fiona" "is" "red" "-")
Fiona is smart.
("Fiona" "is" "smart" "+")
If someone is smart and not white then they are not big.
((("someone" "is" "smart" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "big" "-"))
Fiona is not red.
True
1
proof
[(triple11)]
("Fiona" "is" "red" "-")
triple11
Bob is not white.
False
1
inv-proof
[(triple4)]
("Bob" "is" "white" "-")
triple4
Dave is not big.
True
3
proof
[(((triple8 triple9) -> rule1))]
("Dave" "is" "big" "-")
((triple8 triple9) -> (rule1 % int1))
Dave is not big.
("Dave" "is" "big" "-")
int1
Dave is big.
False
3
inv-proof
[(((triple8 triple9) -> rule1))]
("Dave" "is" "big" "+")
((triple8 triple9) -> (rule1 % int1))
Dave is not big.
("Dave" "is" "big" "-")
int1
Fiona is not nice.
Unknown
inv-random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "-")
Fiona is white.
Unknown
random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "+")
Bob is not smart.
Unknown
inv-random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
@0: Bob is big.[(triple1)] Bob is nice.[(triple3)] Bob is not cold.[(triple2)] Bob is white.[(triple4)] Dave is not nice.[(triple5)] Dave is not red.[(triple7)] Dave is not white.[(triple9)] Dave is quiet.[(triple6)] Dave is smart.[(triple8)] Fiona is not red.[(triple11)] Fiona is quiet.[(triple10)] Fiona is smart.[(triple12)] @1: Dave is not big.[(((triple8 triple9) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Bob is not cold.
("Bob" "is" "cold" "-")
triple2
Bob is white.
("Bob" "is" "white" "+")
triple4
Dave is not nice.
("Dave" "is" "nice" "-")
triple5
Dave is not red.
("Dave" "is" "red" "-")
triple7
Dave is not white.
("Dave" "is" "white" "-")
triple9
Dave is quiet.
("Dave" "is" "quiet" "+")
triple6
Dave is smart.
("Dave" "is" "smart" "+")
triple8
Fiona is not red.
("Fiona" "is" "red" "-")
triple11
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple10
Fiona is smart.
("Fiona" "is" "smart" "+")
triple12
Dave is not big.
("Dave" "is" "big" "-")
((triple8 triple9) -> (rule1 % int1))
Dave is not big.
("Dave" "is" "big" "-")
int1