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