Charlie is round. Fiona is big. Harry is kind. If Fiona is round then Fiona is not big. If someone is kind then they are big. White people are big. If someone is big then they are kind. If Fiona is round then Fiona is not white. All kind people are not cold.
Charlie is round.
("Charlie" "is" "round" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Harry is kind.
("Harry" "is" "kind" "+")
If Fiona is round then Fiona is not big.
((("Fiona" "is" "round" "+")) -> ("Fiona" "is" "big" "-"))
If someone is kind then they are big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
White people are big.
((("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
If someone is big then they are kind.
((("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
If Fiona is round then Fiona is not white.
((("Fiona" "is" "round" "+")) -> ("Fiona" "is" "white" "-"))
All kind people are not cold.
((("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "-"))
Charlie is round.
True
1
proof
[(triple1)]
("Charlie" "is" "round" "+")
triple1
Harry is not kind.
False
1
inv-proof
[(triple3)]
("Harry" "is" "kind" "-")
triple3
Harry is big.
True
2
proof
[(((triple3) -> rule2))]
("Harry" "is" "big" "+")
((triple3) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is not big.
False
2
inv-proof
[(((triple3) -> rule2))]
("Harry" "is" "big" "-")
((triple3) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Fiona is not cold.
True
3
proof
[(((((triple2) -> rule4)) -> rule6))]
("Fiona" "is" "cold" "-")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is not cold.
("Fiona" "is" "cold" "-")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is cold.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule6))]
("Fiona" "is" "cold" "+")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is not cold.
("Fiona" "is" "cold" "-")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Charlie is not kind.
Unknown
inv-rconc
[@2: Charlie is kind.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("Charlie" "is" "kind" "-")
Charlie is big.
Unknown
rconc
[@3: Charlie is big.[CWA. Example of deepest failure = (rule2 <- rule4 <- rule3 <- FAIL)]]
("Charlie" "is" "big" "+")
Fiona is not quiet.
Unknown
inv-random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
Fiona is not white.
Unknown
inv-random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
@0: Charlie is round.[(triple1)] Fiona is big.[(triple2)] Harry is kind.[(triple3)] @1: Fiona is kind.[(((triple2) -> rule4))] Harry is big.[(((triple3) -> rule2))] Harry is not cold.[(((triple3) -> rule6))] @2: Fiona is not cold.[(((((triple2) -> rule4)) -> rule6))]
Charlie is round.
("Charlie" "is" "round" "+")
triple1
Fiona is big.
("Fiona" "is" "big" "+")
triple2
Harry is kind.
("Harry" "is" "kind" "+")
triple3
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple2) -> (rule4 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple3) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is not cold.
("Harry" "is" "cold" "-")
((triple3) -> (rule6 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Fiona is not cold.
("Fiona" "is" "cold" "-")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is not cold.
("Fiona" "is" "cold" "-")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2