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