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