Bob is blue. Bob is not quiet. Bob is red. Charlie is big. Charlie is kind. Charlie is quiet. Charlie is red. Charlie is rough. Dave is big. Dave is not blue. Dave is not kind. Dave is red. Dave is white. Fiona is big. Fiona is white. If Dave is blue then Dave is white. If someone is big and not blue then they are quiet. If someone is quiet and rough then they are big. Rough people are white. If someone is blue then they are rough. If someone is quiet and not big then they are not kind.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is not quiet.
("Bob" "is" "quiet" "-")
Bob is red.
("Bob" "is" "red" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is not blue.
("Dave" "is" "blue" "-")
Dave is not kind.
("Dave" "is" "kind" "-")
Dave is red.
("Dave" "is" "red" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is white.
("Fiona" "is" "white" "+")
If Dave is blue then Dave is white.
((("Dave" "is" "blue" "+")) -> ("Dave" "is" "white" "+"))
If someone is big and not blue then they are quiet.
((("someone" "is" "big" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "quiet" "+"))
If someone is quiet and rough then they are big.
((("someone" "is" "quiet" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
Rough people are white.
((("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
If someone is blue then they are rough.
((("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
If someone is quiet and not big then they are not kind.
((("someone" "is" "quiet" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "kind" "-"))
Bob is not quiet.
True
1
proof
[(triple2)]
("Bob" "is" "quiet" "-")
triple2
Charlie is not red.
False
1
inv-proof
[(triple7)]
("Charlie" "is" "red" "-")
triple7
Dave is quiet.
True
3
proof
[(((triple9 triple10) -> rule2))]
("Dave" "is" "quiet" "+")
((triple9 triple10) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Charlie is not white.
False
2
inv-proof
[(((triple8) -> rule4))]
("Charlie" "is" "white" "-")
((triple8) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Bob is white.
True
3
proof
[(((((triple1) -> rule5)) -> rule4))]
("Bob" "is" "white" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is not white.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule4))]
("Bob" "is" "white" "-")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Fiona is not rough.
Unknown
inv-rconc
[@1: Fiona is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "rough" "-")
Fiona is quiet.
Unknown
rconc
[@1: Fiona is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "quiet" "+")
Bob is not big.
Unknown
inv-rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "big" "-")
Fiona is blue.
Unknown
random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "+")
Bob is not kind.
Unknown
inv-random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "-")
Fiona is red.
Unknown
random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "+")
@0: Bob is blue.[(triple1)] Bob is not quiet.[(triple2)] Bob is red.[(triple3)] Charlie is big.[(triple4 OR ((triple6 triple8) -> rule3))] Charlie is kind.[(triple5)] Charlie is quiet.[(triple6)] Charlie is red.[(triple7)] Charlie is rough.[(triple8)] Dave is big.[(triple9)] Dave is not blue.[(triple10)] Dave is not kind.[(triple11)] Dave is red.[(triple12)] Dave is white.[(triple13)] Fiona is big.[(triple14)] Fiona is white.[(triple15)] @1: Bob is rough.[(((triple1) -> rule5))] Charlie is white.[(((triple8) -> rule4))] Dave is quiet.[(((triple9 triple10) -> rule2))] @2: Bob is white.[(((((triple1) -> rule5)) -> rule4))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is not quiet.
("Bob" "is" "quiet" "-")
triple2
Bob is red.
("Bob" "is" "red" "+")
triple3
Charlie is big.
("Charlie" "is" "big" "+")
triple4
((triple6 triple8) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple5
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple6
Charlie is red.
("Charlie" "is" "red" "+")
triple7
Charlie is rough.
("Charlie" "is" "rough" "+")
triple8
Dave is big.
("Dave" "is" "big" "+")
triple9
Dave is not blue.
("Dave" "is" "blue" "-")
triple10
Dave is not kind.
("Dave" "is" "kind" "-")
triple11
Dave is red.
("Dave" "is" "red" "+")
triple12
Dave is white.
("Dave" "is" "white" "+")
triple13
Fiona is big.
("Fiona" "is" "big" "+")
triple14
Fiona is white.
("Fiona" "is" "white" "+")
triple15
Bob is rough.
("Bob" "is" "rough" "+")
((triple1) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((triple8) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple9 triple10) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2