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