Charlie is cold. Charlie is nice. Dave is nice. Dave is round. Dave is white. Fiona is big. Fiona is cold. Fiona is smart. Fiona is white. Harry is white. If something is big and not nice then it is cold. If Harry is kind and Harry is white then Harry is round. If Harry is white then Harry is kind. If Harry is cold then Harry is kind. If something is nice and not cold then it is smart. Smart things are not round.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Harry is white.
("Harry" "is" "white" "+")
If something is big and not nice then it is cold.
((("something" "is" "big" "+") ("something" "is" "nice" "~")) -> ("something" "is" "cold" "+"))
If Harry is kind and Harry is white then Harry is round.
((("Harry" "is" "kind" "+") ("Harry" "is" "white" "+")) -> ("Harry" "is" "round" "+"))
If Harry is white then Harry is kind.
((("Harry" "is" "white" "+")) -> ("Harry" "is" "kind" "+"))
If Harry is cold then Harry is kind.
((("Harry" "is" "cold" "+")) -> ("Harry" "is" "kind" "+"))
If something is nice and not cold then it is smart.
((("something" "is" "nice" "+") ("something" "is" "cold" "~")) -> ("something" "is" "smart" "+"))
Smart things are not round.
((("something" "is" "smart" "+")) -> ("something" "is" "round" "-"))
Fiona is big.
True
1
proof
[(triple6)]
("Fiona" "is" "big" "+")
triple6
Charlie is not nice.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "nice" "-")
triple2
Fiona is not round.
True
2
proof
[(((triple8) -> rule6))]
("Fiona" "is" "round" "-")
((triple8) -> (rule6 % int1))
Fiona is not round.
("Fiona" "is" "round" "-")
int1
Fiona is round.
False
2
inv-proof
[(((triple8) -> rule6))]
("Fiona" "is" "round" "+")
((triple8) -> (rule6 % int1))
Fiona is not round.
("Fiona" "is" "round" "-")
int1
Harry is round.
True
4
proof
[(((((triple10) -> rule3) triple10) -> rule2))]
("Harry" "is" "round" "+")
((((triple10) -> (rule3 % int2)) triple10) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is not round.
False
4
inv-proof
[(((((triple10) -> rule3) triple10) -> rule2))]
("Harry" "is" "round" "-")
((((triple10) -> (rule3 % int2)) triple10) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Dave is not smart.
Unknown
inv-rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "smart" "-")
Charlie is smart.
Unknown
rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "smart" "+")
Dave is not cold.
Unknown
inv-rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "cold" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
@0: Charlie is cold.[(triple1)] Charlie is nice.[(triple2)] Dave is nice.[(triple3)] Dave is round.[(triple4)] Dave is white.[(triple5)] Fiona is big.[(triple6)] Fiona is cold.[(triple7)] Fiona is smart.[(triple8)] Fiona is white.[(triple9)] Harry is white.[(triple10)] @1: Fiona is not round.[(((triple8) -> rule6))] Harry is kind.[(((triple10) -> rule3))] @2: Harry is round.[(((((triple10) -> rule3) triple10) -> rule2))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Dave is round.
("Dave" "is" "round" "+")
triple4
Dave is white.
("Dave" "is" "white" "+")
triple5
Fiona is big.
("Fiona" "is" "big" "+")
triple6
Fiona is cold.
("Fiona" "is" "cold" "+")
triple7
Fiona is smart.
("Fiona" "is" "smart" "+")
triple8
Fiona is white.
("Fiona" "is" "white" "+")
triple9
Harry is white.
("Harry" "is" "white" "+")
triple10
Fiona is not round.
("Fiona" "is" "round" "-")
((triple8) -> (rule6 % int1))
Fiona is not round.
("Fiona" "is" "round" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((triple10) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((((triple10) -> (rule3 % int2)) triple10) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2