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