Charlie is blue. Fiona is not round. Harry is nice. If Harry is white then Harry is round. Big things are not blue. If something is nice and not round then it is not big. All quiet, nice things are big. If something is big then it is quiet. Nice, blue things are not quiet. If something is smart then it is not quiet. All blue things are nice.
Charlie is blue.
("Charlie" "is" "blue" "+")
Fiona is not round.
("Fiona" "is" "round" "-")
Harry is nice.
("Harry" "is" "nice" "+")
If Harry is white then Harry is round.
((("Harry" "is" "white" "+")) -> ("Harry" "is" "round" "+"))
Big things are not blue.
((("something" "is" "big" "+")) -> ("something" "is" "blue" "-"))
If something is nice and not round then it is not big.
((("something" "is" "nice" "+") ("something" "is" "round" "~")) -> ("something" "is" "big" "-"))
All quiet, nice things are big.
((("something" "is" "quiet" "+") ("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
If something is big then it is quiet.
((("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
Nice, blue things are not quiet.
((("something" "is" "nice" "+") ("something" "is" "blue" "+")) -> ("something" "is" "quiet" "-"))
If something is smart then it is not quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "-"))
All blue things are nice.
((("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
Charlie is blue.
True
1
proof
[(triple1)]
("Charlie" "is" "blue" "+")
triple1
Harry is not nice.
False
1
inv-proof
[(triple3)]
("Harry" "is" "nice" "-")
triple3
Charlie is nice.
True
2
proof
[(((triple1) -> rule8))]
("Charlie" "is" "nice" "+")
((triple1) -> (rule8 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is not nice.
False
2
inv-proof
[(((triple1) -> rule8))]
("Charlie" "is" "nice" "-")
((triple1) -> (rule8 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is not quiet.
True
4
proof
[(((((triple1) -> rule8) triple1) -> rule6))]
("Charlie" "is" "quiet" "-")
((((triple1) -> (rule8 % int2)) triple1) -> (rule6 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is quiet.
False
4
inv-proof
[(((((triple1) -> rule8) triple1) -> rule6))]
("Charlie" "is" "quiet" "+")
((((triple1) -> (rule8 % int2)) triple1) -> (rule6 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Fiona is not big.
Unknown
inv-rconc
[@2: Fiona is big.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("Fiona" "is" "big" "-")
Harry is round.
Unknown
rconc
[@1: Harry is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "round" "+")
Harry is not quiet.
Unknown
inv-rconc
[@2: Harry is quiet.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("Harry" "is" "quiet" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
Fiona is not blue.
Unknown
inv-random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
@0: Charlie is blue.[(triple1)] Fiona is not round.[(triple2)] Harry is nice.[(triple3)] @1: Charlie is nice.[(((triple1) -> rule8))] @2: Charlie is not quiet.[(((((triple1) -> rule8) triple1) -> rule6))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Fiona is not round.
("Fiona" "is" "round" "-")
triple2
Harry is nice.
("Harry" "is" "nice" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple1) -> (rule8 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
((((triple1) -> (rule8 % int2)) triple1) -> (rule6 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2