Charlie is nice. Erin is nice. Erin is young. Fiona is cold. Fiona is green. Fiona is kind. Harry is round. Quiet things are round. If something is nice then it is quiet.
Charlie is nice.
("Charlie" "is" "nice" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is young.
("Erin" "is" "young" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Harry is round.
("Harry" "is" "round" "+")
Quiet things are round.
((("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
If something is nice then it is quiet.
((("something" "is" "nice" "+")) -> ("something" "is" "quiet" "+"))
Charlie is nice.
True
1
proof
[(triple1)]
("Charlie" "is" "nice" "+")
triple1
Erin is not nice.
False
1
inv-proof
[(triple2)]
("Erin" "is" "nice" "-")
triple2
Erin is quiet.
True
2
proof
[(((triple2) -> rule2))]
("Erin" "is" "quiet" "+")
((triple2) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is not quiet.
False
2
inv-proof
[(((triple2) -> rule2))]
("Erin" "is" "quiet" "-")
((triple2) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is round.
True
3
proof
[(((((triple2) -> rule2)) -> rule1))]
("Erin" "is" "round" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Charlie is not round.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule1))]
("Charlie" "is" "round" "-")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Fiona is not quiet.
Unknown
inv-rconc
[@1: Fiona is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "quiet" "-")
Fiona is round.
Unknown
rconc
[@2: Fiona is round.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Fiona" "is" "round" "+")
Harry is not quiet.
Unknown
inv-rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "quiet" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
@0: Charlie is nice.[(triple1)] Erin is nice.[(triple2)] Erin is young.[(triple3)] Fiona is cold.[(triple4)] Fiona is green.[(triple5)] Fiona is kind.[(triple6)] Harry is round.[(triple7)] @1: Charlie is quiet.[(((triple1) -> rule2))] Erin is quiet.[(((triple2) -> rule2))] @2: Charlie is round.[(((((triple1) -> rule2)) -> rule1))] Erin is round.[(((((triple2) -> rule2)) -> rule1))]
Charlie is nice.
("Charlie" "is" "nice" "+")
triple1
Erin is nice.
("Erin" "is" "nice" "+")
triple2
Erin is young.
("Erin" "is" "young" "+")
triple3
Fiona is cold.
("Fiona" "is" "cold" "+")
triple4
Fiona is green.
("Fiona" "is" "green" "+")
triple5
Fiona is kind.
("Fiona" "is" "kind" "+")
triple6
Harry is round.
("Harry" "is" "round" "+")
triple7
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple1) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple2) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2