Charlie is not cold. Fiona is nice. Gary is quiet. If someone is quiet then they are cold. If someone is furry then they are cold. All young people are not smart. If someone is nice and furry then they are smart. All quiet, kind people are smart. If Charlie is not furry then Charlie is young. If someone is cold then they are kind. All smart, young people are kind.
Charlie is not cold.
("Charlie" "is" "cold" "-")
Fiona is nice.
("Fiona" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
If someone is quiet then they are cold.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "+"))
If someone is furry then they are cold.
((("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "+"))
All young people are not smart.
((("someone" "is" "young" "+")) -> ("someone" "is" "smart" "-"))
If someone is nice and furry then they are smart.
((("someone" "is" "nice" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "+"))
All quiet, kind people are smart.
((("someone" "is" "quiet" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
If Charlie is not furry then Charlie is young.
((("Charlie" "is" "furry" "~")) -> ("Charlie" "is" "young" "+"))
If someone is cold then they are kind.
((("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
All smart, young people are kind.
((("someone" "is" "smart" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
Charlie is not cold.
True
1
proof
[(triple1)]
("Charlie" "is" "cold" "-")
triple1
Fiona is not nice.
False
1
inv-proof
[(triple2)]
("Fiona" "is" "nice" "-")
triple2
Gary is cold.
True
2
proof
[(((triple3) -> rule1))]
("Gary" "is" "cold" "+")
((triple3) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is not cold.
False
2
inv-proof
[(((triple3) -> rule1))]
("Gary" "is" "cold" "-")
((triple3) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is kind.
True
3
proof
[(((((triple3) -> rule1)) -> rule7))]
("Gary" "is" "kind" "+")
((((triple3) -> (rule1 % int2))) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is not kind.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule7))]
("Gary" "is" "kind" "-")
((((triple3) -> (rule1 % int2))) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is smart.
True
5
proof
[(((triple3 ((((triple3) -> rule1)) -> rule7)) -> rule5))]
("Gary" "is" "smart" "+")
((triple3 ((((triple3) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is not smart.
False
5
inv-proof
[(((triple3 ((((triple3) -> rule1)) -> rule7)) -> rule5))]
("Gary" "is" "smart" "-")
((triple3 ((((triple3) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Fiona is not kind.
Unknown
inv-rconc
[@2: Fiona is kind.[CWA. Example of deepest failure = (rule7 <- rule1 <- FAIL)]]
("Fiona" "is" "kind" "-")
Charlie is smart.
Unknown
rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "smart" "+")
Fiona is not smart.
Unknown
inv-rconc
[@1: Fiona is smart.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "smart" "-")
Fiona is cold.
Unknown
rconc
[@1: Fiona is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "cold" "+")
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
Gary is not furry.
Unknown
inv-random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
@0: Charlie is not cold.[(triple1)] Fiona is nice.[(triple2)] Gary is quiet.[(triple3)] @1: Gary is cold.[(((triple3) -> rule1))] @2: Gary is kind.[(((((triple3) -> rule1)) -> rule7))] @3: Gary is smart.[(((triple3 ((((triple3) -> rule1)) -> rule7)) -> rule5))]
Charlie is not cold.
("Charlie" "is" "cold" "-")
triple1
Fiona is nice.
("Fiona" "is" "nice" "+")
triple2
Gary is quiet.
("Gary" "is" "quiet" "+")
triple3
Gary is cold.
("Gary" "is" "cold" "+")
((triple3) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((((triple3) -> (rule1 % int2))) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
((triple3 ((((triple3) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3