Charlie is cold. Dave is smart. Gary is quiet. Harry is cold. Big, smart people are cold. If someone is furry and big then they are green. Smart, quiet people are furry. All smart, cold people are quiet. If Dave is green and Dave is cold then Dave is quiet. If someone is cold then they are smart.
Charlie is cold.
("Charlie" "is" "cold" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Big, smart people are cold.
((("someone" "is" "big" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
If someone is furry and big then they are green.
((("someone" "is" "furry" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
Smart, quiet people are furry.
((("someone" "is" "smart" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "furry" "+"))
All smart, cold people are quiet.
((("someone" "is" "smart" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
If Dave is green and Dave is cold then Dave is quiet.
((("Dave" "is" "green" "+") ("Dave" "is" "cold" "+")) -> ("Dave" "is" "quiet" "+"))
If someone is cold then they are smart.
((("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
Dave is smart.
True
1
proof
[(triple2)]
("Dave" "is" "smart" "+")
triple2
Harry is not cold.
False
1
inv-proof
[(triple4)]
("Harry" "is" "cold" "-")
triple4
Charlie is smart.
True
2
proof
[(((triple1) -> rule6))]
("Charlie" "is" "smart" "+")
((triple1) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Harry is not smart.
False
2
inv-proof
[(((triple4) -> rule6))]
("Harry" "is" "smart" "-")
((triple4) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is quiet.
True
4
proof
[(((((triple4) -> rule6) triple4) -> rule4))]
("Harry" "is" "quiet" "+")
((((triple4) -> (rule6 % int2)) triple4) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Charlie is not quiet.
False
4
inv-proof
[(((((triple1) -> rule6) triple1) -> rule4))]
("Charlie" "is" "quiet" "-")
((((triple1) -> (rule6 % int2)) triple1) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is not green.
Unknown
inv-rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "green" "-")
Gary is green.
Unknown
rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "green" "+")
Gary is not furry.
Unknown
inv-rconc
[@3: Gary is furry.[CWA. Example of deepest failure = (rule3 <- rule6 <- rule1 <- FAIL)]]
("Gary" "is" "furry" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
@0: Charlie is cold.[(triple1)] Dave is smart.[(triple2)] Gary is quiet.[(triple3)] Harry is cold.[(triple4)] @1: Charlie is smart.[(((triple1) -> rule6))] Harry is smart.[(((triple4) -> rule6))] @2: Charlie is quiet.[(((((triple1) -> rule6) triple1) -> rule4))] Harry is quiet.[(((((triple4) -> rule6) triple4) -> rule4))] @3: Charlie is furry.[(((((triple1) -> rule6) ((((triple1) -> rule6) triple1) -> rule4)) -> rule3))] Harry is furry.[(((((triple4) -> rule6) ((((triple4) -> rule6) triple4) -> rule4)) -> rule3))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Dave is smart.
("Dave" "is" "smart" "+")
triple2
Gary is quiet.
("Gary" "is" "quiet" "+")
triple3
Harry is cold.
("Harry" "is" "cold" "+")
triple4
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple1) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple4) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((triple1) -> (rule6 % int2)) triple1) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
((((triple4) -> (rule6 % int2)) triple4) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
((((triple1) -> (rule6 % int3)) ((((triple1) -> (rule6 % int3)) triple1) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
((((triple4) -> (rule6 % int3)) ((((triple4) -> (rule6 % int3)) triple4) -> (rule4 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3