Anne is nice. Anne is quiet. Anne is smart. Anne is white. Dave is big. Dave is blue. Dave is nice. Dave is quiet. Dave is rough. Dave is smart. Fiona is big. Fiona is blue. Fiona is nice. Fiona is quiet. Fiona is rough. Fiona is white. Nice people are blue. If Dave is smart and Dave is white then Dave is nice. Quiet, big people are blue.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Nice people are blue.
((("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
If Dave is smart and Dave is white then Dave is nice.
((("Dave" "is" "smart" "+") ("Dave" "is" "white" "+")) -> ("Dave" "is" "nice" "+"))
Quiet, big people are blue.
((("someone" "is" "quiet" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
Anne is white.
True
1
proof
[(triple4)]
("Anne" "is" "white" "+")
triple4
Dave is not big.
False
1
inv-proof
[(triple5)]
("Dave" "is" "big" "-")
triple5
Anne is blue.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "blue" "+")
((triple1) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is not blue.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "blue" "-")
((triple1) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
Anne is not rough.
Unknown
inv-random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
@0: Anne is nice.[(triple1)] Anne is quiet.[(triple2)] Anne is smart.[(triple3)] Anne is white.[(triple4)] Dave is big.[(triple5)] Dave is blue.[(triple6 OR ((triple7) -> rule1) OR ((triple8 triple5) -> rule3))] Dave is nice.[(triple7)] Dave is quiet.[(triple8)] Dave is rough.[(triple9)] Dave is smart.[(triple10)] Fiona is big.[(triple11)] Fiona is blue.[(triple12 OR ((triple13) -> rule1) OR ((triple14 triple11) -> rule3))] Fiona is nice.[(triple13)] Fiona is quiet.[(triple14)] Fiona is rough.[(triple15)] Fiona is white.[(triple16)] @1: Anne is blue.[(((triple1) -> rule1))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Anne is smart.
("Anne" "is" "smart" "+")
triple3
Anne is white.
("Anne" "is" "white" "+")
triple4
Dave is big.
("Dave" "is" "big" "+")
triple5
Dave is blue.
("Dave" "is" "blue" "+")
triple6
((triple7) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((triple8 triple5) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
triple7
Dave is quiet.
("Dave" "is" "quiet" "+")
triple8
Dave is rough.
("Dave" "is" "rough" "+")
triple9
Dave is smart.
("Dave" "is" "smart" "+")
triple10
Fiona is big.
("Fiona" "is" "big" "+")
triple11
Fiona is blue.
("Fiona" "is" "blue" "+")
triple12
((triple13) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
((triple14 triple11) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
triple13
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple14
Fiona is rough.
("Fiona" "is" "rough" "+")
triple15
Fiona is white.
("Fiona" "is" "white" "+")
triple16
Anne is blue.
("Anne" "is" "blue" "+")
((triple1) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1