Bob is round. Fiona is green. Gary is blue. Harry is green. Harry is not red. Harry is not round. Harry is young. If something is nice and red then it is white. All red things are white. All young, round things are not red. Round things are red. If Harry is red and Harry is nice then Harry is white. If something is blue then it is nice. Blue, nice things are green. All young, red things are green. If something is white and round then it is blue.
Bob is round.
("Bob" "is" "round" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is not red.
("Harry" "is" "red" "-")
Harry is not round.
("Harry" "is" "round" "-")
Harry is young.
("Harry" "is" "young" "+")
If something is nice and red then it is white.
((("something" "is" "nice" "+") ("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
All red things are white.
((("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
All young, round things are not red.
((("something" "is" "young" "+") ("something" "is" "round" "+")) -> ("something" "is" "red" "-"))
Round things are red.
((("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
If Harry is red and Harry is nice then Harry is white.
((("Harry" "is" "red" "+") ("Harry" "is" "nice" "+")) -> ("Harry" "is" "white" "+"))
If something is blue then it is nice.
((("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
Blue, nice things are green.
((("something" "is" "blue" "+") ("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
All young, red things are green.
((("something" "is" "young" "+") ("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
If something is white and round then it is blue.
((("something" "is" "white" "+") ("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
Harry is not round.
True
1
proof
[(triple6)]
("Harry" "is" "round" "-")
triple6
Harry is not green.
False
1
inv-proof
[(triple4)]
("Harry" "is" "green" "-")
triple4
Bob is red.
True
2
proof
[(((triple1) -> rule4))]
("Bob" "is" "red" "+")
((triple1) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Gary is not nice.
False
2
inv-proof
[(((triple3) -> rule6))]
("Gary" "is" "nice" "-")
((triple3) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Bob is white.
True
3
proof
[(((((triple1) -> rule4)) -> rule2))]
("Bob" "is" "white" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is not white.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule2))]
("Bob" "is" "white" "-")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is blue.
True
5
proof
[(((((((triple1) -> rule4)) -> rule2) triple1) -> rule9))]
("Bob" "is" "blue" "+")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2)) triple1) -> (rule9 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is not blue.
False
5
inv-proof
[(((((((triple1) -> rule4)) -> rule2) triple1) -> rule9))]
("Bob" "is" "blue" "-")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2)) triple1) -> (rule9 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is nice.
True
6
proof
[(((((((((triple1) -> rule4)) -> rule2) triple1) -> rule9)) -> rule6))]
("Bob" "is" "nice" "+")
((((((((triple1) -> (rule4 % int4))) -> (rule2 % int3)) triple1) -> (rule9 % int2))) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4
Bob is not nice.
False
6
inv-proof
[(((((((((triple1) -> rule4)) -> rule2) triple1) -> rule9)) -> rule6))]
("Bob" "is" "nice" "-")
((((((((triple1) -> (rule4 % int4))) -> (rule2 % int3)) triple1) -> (rule9 % int2))) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4
Bob is green.
True
12
proof
[(((((((((triple1) -> rule4)) -> rule2) triple1) -> rule9) ((((((((triple1) -> rule4)) -> rule2) triple1) -> rule9)) -> rule6)) -> rule7))]
("Bob" "is" "green" "+")
((((((((triple1) -> (rule4 % int5))) -> (rule2 % int4)) triple1) -> (rule9 % int3)) ((((((((triple1) -> (rule4 % int5))) -> (rule2 % int4)) triple1) -> (rule9 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Bob is red.
("Bob" "is" "red" "+")
int5
Bob is not green.
False
12
inv-proof
[(((((((((triple1) -> rule4)) -> rule2) triple1) -> rule9) ((((((((triple1) -> rule4)) -> rule2) triple1) -> rule9)) -> rule6)) -> rule7))]
("Bob" "is" "green" "-")
((((((((triple1) -> (rule4 % int5))) -> (rule2 % int4)) triple1) -> (rule9 % int3)) ((((((((triple1) -> (rule4 % int5))) -> (rule2 % int4)) triple1) -> (rule9 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Bob is red.
("Bob" "is" "red" "+")
int5
Harry is not blue.
Unknown
inv-rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("Harry" "is" "blue" "-")
Fiona is nice.
Unknown
rconc
[@2: Fiona is nice.[CWA. Example of deepest failure = (rule6 <- rule9 <- FAIL)]]
("Fiona" "is" "nice" "+")
Fiona is not red.
Unknown
inv-rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "red" "-")
Fiona is blue.
Unknown
rconc
[@1: Fiona is blue.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("Fiona" "is" "blue" "+")
Harry is not nice.
Unknown
inv-rconc
[@2: Harry is nice.[CWA. Example of deepest failure = (rule6 <- rule9 <- FAIL)]]
("Harry" "is" "nice" "-")
Harry is white.
Unknown
rconc
[@1: Harry is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "white" "+")
Bob is not young.
Unknown
inv-random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
Gary is not round.
Unknown
inv-random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "-")
Fiona is young.
Unknown
random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "+")
@0: Bob is round.[(triple1)] Fiona is green.[(triple2)] Gary is blue.[(triple3)] Harry is green.[(triple4)] Harry is not red.[(triple5)] Harry is not round.[(triple6)] Harry is young.[(triple7)] @1: Bob is red.[(((triple1) -> rule4))] Gary is nice.[(((triple3) -> rule6))] @2: Bob is white.[(((((triple1) -> rule4)) -> rule2))] Gary is green.[(((triple3 ((triple3) -> rule6)) -> rule7))] @3: Bob is blue.[(((((((triple1) -> rule4)) -> rule2) triple1) -> rule9))] @4: Bob is nice.[(((((((((triple1) -> rule4)) -> rule2) triple1) -> rule9)) -> rule6))] @5: Bob is green.[(((((((((triple1) -> rule4)) -> rule2) triple1) -> rule9) ((((((((triple1) -> rule4)) -> rule2) triple1) -> rule9)) -> rule6)) -> rule7))]
Bob is round.
("Bob" "is" "round" "+")
triple1
Fiona is green.
("Fiona" "is" "green" "+")
triple2
Gary is blue.
("Gary" "is" "blue" "+")
triple3
Harry is green.
("Harry" "is" "green" "+")
triple4
Harry is not red.
("Harry" "is" "red" "-")
triple5
Harry is not round.
("Harry" "is" "round" "-")
triple6
Harry is young.
("Harry" "is" "young" "+")
triple7
Bob is red.
("Bob" "is" "red" "+")
((triple1) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((triple3) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
((triple3 ((triple3) -> (rule6 % int2))) -> (rule7 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2)) triple1) -> (rule9 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
((((((((triple1) -> (rule4 % int4))) -> (rule2 % int3)) triple1) -> (rule9 % int2))) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4
Bob is green.
("Bob" "is" "green" "+")
((((((((triple1) -> (rule4 % int5))) -> (rule2 % int4)) triple1) -> (rule9 % int3)) ((((((((triple1) -> (rule4 % int5))) -> (rule2 % int4)) triple1) -> (rule9 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Bob is red.
("Bob" "is" "red" "+")
int5