Charlie is cold. Charlie is rough. Erin is nice. Erin is not quiet. Harry is cold. Harry is not smart. Harry is white. If something is white and big then it is quiet. If something is white then it is big.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is not quiet.
("Erin" "is" "quiet" "-")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is not smart.
("Harry" "is" "smart" "-")
Harry is white.
("Harry" "is" "white" "+")
If something is white and big then it is quiet.
((("something" "is" "white" "+") ("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
If something is white then it is big.
((("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
Charlie is rough.
True
1
proof
[(triple2)]
("Charlie" "is" "rough" "+")
triple2
Harry is not white.
False
1
inv-proof
[(triple7)]
("Harry" "is" "white" "-")
triple7
Harry is big.
True
2
proof
[(((triple7) -> rule2))]
("Harry" "is" "big" "+")
((triple7) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is not big.
False
2
inv-proof
[(((triple7) -> rule2))]
("Harry" "is" "big" "-")
((triple7) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is quiet.
True
4
proof
[(((triple7 ((triple7) -> rule2)) -> rule1))]
("Harry" "is" "quiet" "+")
((triple7 ((triple7) -> (rule2 % int2))) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not quiet.
False
4
inv-proof
[(((triple7 ((triple7) -> rule2)) -> rule1))]
("Harry" "is" "quiet" "-")
((triple7 ((triple7) -> (rule2 % int2))) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Erin is not big.
Unknown
inv-rconc
[@1: Erin is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "big" "-")
Charlie is quiet.
Unknown
rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "quiet" "+")
Charlie is not big.
Unknown
inv-rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "big" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
Erin is not rough.
Unknown
inv-random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "-")
Erin is white.
Unknown
random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "+")
@0: Charlie is cold.[(triple1)] Charlie is rough.[(triple2)] Erin is nice.[(triple3)] Erin is not quiet.[(triple4)] Harry is cold.[(triple5)] Harry is not smart.[(triple6)] Harry is white.[(triple7)] @1: Harry is big.[(((triple7) -> rule2))] @2: Harry is quiet.[(((triple7 ((triple7) -> rule2)) -> rule1))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple2
Erin is nice.
("Erin" "is" "nice" "+")
triple3
Erin is not quiet.
("Erin" "is" "quiet" "-")
triple4
Harry is cold.
("Harry" "is" "cold" "+")
triple5
Harry is not smart.
("Harry" "is" "smart" "-")
triple6
Harry is white.
("Harry" "is" "white" "+")
triple7
Harry is big.
("Harry" "is" "big" "+")
((triple7) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple7 ((triple7) -> (rule2 % int2))) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2