Charlie is quiet. Fiona is smart. Harry is kind. All big, smart people are quiet. Kind people are big. If Harry is big then Harry is smart.
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Harry is kind.
("Harry" "is" "kind" "+")
All big, smart people are quiet.
((("someone" "is" "big" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
Kind people are big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
If Harry is big then Harry is smart.
((("Harry" "is" "big" "+")) -> ("Harry" "is" "smart" "+"))
Harry is kind.
True
1
proof
[(triple3)]
("Harry" "is" "kind" "+")
triple3
Charlie is not quiet.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "quiet" "-")
triple1
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
Harry is smart.
True
3
proof
[(((((triple3) -> rule2)) -> rule3))]
("Harry" "is" "smart" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not smart.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule3))]
("Harry" "is" "smart" "-")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is quiet.
True
6
proof
[(((((triple3) -> rule2) ((((triple3) -> rule2)) -> rule3)) -> rule1))]
("Harry" "is" "quiet" "+")
((((triple3) -> (rule2 % int3)) ((((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is not quiet.
False
6
inv-proof
[(((((triple3) -> rule2) ((((triple3) -> rule2)) -> rule3)) -> rule1))]
("Harry" "is" "quiet" "-")
((((triple3) -> (rule2 % int3)) ((((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Charlie is not big.
Unknown
inv-rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "big" "-")
Fiona is big.
Unknown
rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "big" "+")
Fiona is not quiet.
Unknown
inv-rconc
[@2: Fiona is quiet.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Fiona" "is" "quiet" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
Fiona is not kind.
Unknown
inv-random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "-")
Fiona is blue.
Unknown
random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "+")
Harry is not nice.
Unknown
inv-random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
@0: Charlie is quiet.[(triple1)] Fiona is smart.[(triple2)] Harry is kind.[(triple3)] @1: Harry is big.[(((triple3) -> rule2))] @2: Harry is smart.[(((((triple3) -> rule2)) -> rule3))] @3: Harry is quiet.[(((((triple3) -> rule2) ((((triple3) -> rule2)) -> rule3)) -> rule1))]
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple1
Fiona is smart.
("Fiona" "is" "smart" "+")
triple2
Harry is kind.
("Harry" "is" "kind" "+")
triple3
Harry is big.
("Harry" "is" "big" "+")
((triple3) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
((((triple3) -> (rule2 % int3)) ((((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3