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