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