Fiona is not rough. Gary is blue. Gary is cold. All blue people are cold. All cold people are not rough. If someone is cold and not rough then they are young.
Fiona is not rough.
("Fiona" "is" "rough" "-")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
All blue people are cold.
((("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
All cold people are not rough.
((("someone" "is" "cold" "+")) -> ("someone" "is" "rough" "-"))
If someone is cold and not rough then they are young.
((("someone" "is" "cold" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "young" "+"))
Gary is cold.
True
1
proof
[(triple3 OR ((triple2) -> rule1))]
("Gary" "is" "cold" "+")
triple3
((triple2) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is not cold.
False
1
inv-proof
[(triple3 OR ((triple2) -> rule1))]
("Gary" "is" "cold" "-")
triple3
((triple2) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is not rough.
True
2
proof
[(((triple3) -> rule2) OR ((((triple2) -> rule1)) -> rule2))]
("Gary" "is" "rough" "-")
((triple3) -> (rule2 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is rough.
False
2
inv-proof
[(((triple3) -> rule2) OR ((((triple2) -> rule1)) -> rule2))]
("Gary" "is" "rough" "+")
((triple3) -> (rule2 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is young.
True
4
proof
[(((triple3 ((triple3) -> rule2)) -> rule3) OR ((((triple2) -> rule1) ((triple3) -> rule2)) -> rule3) OR ((triple3 ((((triple2) -> rule1)) -> rule2)) -> rule3) OR ((((triple2) -> rule1) ((((triple2) -> rule1)) -> rule2)) -> rule3))]
("Gary" "is" "young" "+")
((triple3 ((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is not rough.
("Gary" "is" "rough" "-")
int2
((((triple2) -> (rule1 % int3)) ((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is not rough.
("Gary" "is" "rough" "-")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
((triple3 ((((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is not rough.
("Gary" "is" "rough" "-")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
((((triple2) -> (rule1 % int3)) ((((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is not rough.
("Gary" "is" "rough" "-")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is not young.
False
4
inv-proof
[(((triple3 ((triple3) -> rule2)) -> rule3) OR ((((triple2) -> rule1) ((triple3) -> rule2)) -> rule3) OR ((triple3 ((((triple2) -> rule1)) -> rule2)) -> rule3) OR ((((triple2) -> rule1) ((((triple2) -> rule1)) -> rule2)) -> rule3))]
("Gary" "is" "young" "-")
((triple3 ((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is not rough.
("Gary" "is" "rough" "-")
int2
((((triple2) -> (rule1 % int3)) ((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is not rough.
("Gary" "is" "rough" "-")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
((triple3 ((((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is not rough.
("Gary" "is" "rough" "-")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
((((triple2) -> (rule1 % int3)) ((((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is not rough.
("Gary" "is" "rough" "-")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Fiona is not young.
Unknown
inv-rconc
[@1: Fiona is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "young" "-")
Fiona is cold.
Unknown
rconc
[@1: Fiona is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "cold" "+")
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Gary is nice.
Unknown
random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "+")
Gary is not smart.
Unknown
inv-random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "-")
Fiona is green.
Unknown
random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "+")
@0: Fiona is not rough.[(triple1)] Gary is blue.[(triple2)] Gary is cold.[(triple3 OR ((triple2) -> rule1))] @1: Gary is not rough.[(((triple3) -> rule2) OR ((((triple2) -> rule1)) -> rule2))] @2: Gary is young.[(((triple3 ((triple3) -> rule2)) -> rule3) OR ((((triple2) -> rule1) ((triple3) -> rule2)) -> rule3) OR ((triple3 ((((triple2) -> rule1)) -> rule2)) -> rule3) OR ((((triple2) -> rule1) ((((triple2) -> rule1)) -> rule2)) -> rule3))]
Fiona is not rough.
("Fiona" "is" "rough" "-")
triple1
Gary is blue.
("Gary" "is" "blue" "+")
triple2
Gary is cold.
("Gary" "is" "cold" "+")
triple3
((triple2) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is not rough.
("Gary" "is" "rough" "-")
((triple3) -> (rule2 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
((triple3 ((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is not rough.
("Gary" "is" "rough" "-")
int2
((((triple2) -> (rule1 % int3)) ((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is not rough.
("Gary" "is" "rough" "-")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
((triple3 ((((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is not rough.
("Gary" "is" "rough" "-")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
((((triple2) -> (rule1 % int3)) ((((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is not rough.
("Gary" "is" "rough" "-")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3