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