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