Fiona is rough. Gary is cold. Harry is rough. All rough people are blue. If Harry is cold and Harry is young then Harry is red. If someone is young then they are not red. Blue people are young. If someone is red and rough then they are round. All red, blue people are round.
Fiona is rough.
("Fiona" "is" "rough" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Harry is rough.
("Harry" "is" "rough" "+")
All rough people are blue.
((("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "+"))
If Harry is cold and Harry is young then Harry is red.
((("Harry" "is" "cold" "+") ("Harry" "is" "young" "+")) -> ("Harry" "is" "red" "+"))
If someone is young then they are not red.
((("someone" "is" "young" "+")) -> ("someone" "is" "red" "-"))
Blue people are young.
((("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
If someone is red and rough then they are round.
((("someone" "is" "red" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "round" "+"))
All red, blue people are round.
((("someone" "is" "red" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
Harry is rough.
True
1
proof
[(triple3)]
("Harry" "is" "rough" "+")
triple3
Fiona is not rough.
False
1
inv-proof
[(triple1)]
("Fiona" "is" "rough" "-")
triple1
Harry is blue.
True
2
proof
[(((triple3) -> rule1))]
("Harry" "is" "blue" "+")
((triple3) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is not blue.
False
2
inv-proof
[(((triple3) -> rule1))]
("Harry" "is" "blue" "-")
((triple3) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is young.
True
3
proof
[(((((triple3) -> rule1)) -> rule4))]
("Harry" "is" "young" "+")
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is not young.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule4))]
("Harry" "is" "young" "-")
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Fiona is not red.
True
4
proof
[(((((((triple1) -> rule1)) -> rule4)) -> rule3))]
("Fiona" "is" "red" "-")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is not red.
("Fiona" "is" "red" "-")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Harry is red.
False
4
inv-proof
[(((((((triple3) -> rule1)) -> rule4)) -> rule3))]
("Harry" "is" "red" "+")
((((((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is not round.
Unknown
inv-rconc
[@1: Harry is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "round" "-")
Fiona is round.
Unknown
rconc
[@1: Fiona is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "round" "+")
Gary is not young.
Unknown
inv-rconc
[@2: Gary is young.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Gary" "is" "young" "-")
Gary is round.
Unknown
rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "round" "+")
Gary is not kind.
Unknown
inv-random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
Fiona is not kind.
Unknown
inv-random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Fiona is rough.[(triple1)] Gary is cold.[(triple2)] Harry is rough.[(triple3)] @1: Fiona is blue.[(((triple1) -> rule1))] Harry is blue.[(((triple3) -> rule1))] @2: Fiona is young.[(((((triple1) -> rule1)) -> rule4))] Harry is young.[(((((triple3) -> rule1)) -> rule4))] @3: Fiona is not red.[(((((((triple1) -> rule1)) -> rule4)) -> rule3))] Harry is not red.[(((((((triple3) -> rule1)) -> rule4)) -> rule3))]
Fiona is rough.
("Fiona" "is" "rough" "+")
triple1
Gary is cold.
("Gary" "is" "cold" "+")
triple2
Harry is rough.
("Harry" "is" "rough" "+")
triple3
Fiona is blue.
("Fiona" "is" "blue" "+")
((triple1) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple3) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Fiona is not red.
("Fiona" "is" "red" "-")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is not red.
("Fiona" "is" "red" "-")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Harry is not red.
("Harry" "is" "red" "-")
((((((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3