Dave is quiet. Fiona is green. If someone is nice and green then they are big. All young people are big. All green people are young. If someone is green then they are young. If someone is big and smart then they are quiet. All big people are green. If someone is cold and quiet then they are smart. If someone is smart then they are nice.
Dave is quiet.
("Dave" "is" "quiet" "+")
Fiona is green.
("Fiona" "is" "green" "+")
If someone is nice and green then they are big.
((("someone" "is" "nice" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
All young people are big.
((("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
All green people are young.
((("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
If someone is green then they are young.
((("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
If someone is big and smart then they are quiet.
((("someone" "is" "big" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
All big people are green.
((("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
If someone is cold and quiet then they are smart.
((("someone" "is" "cold" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
If someone is smart then they are nice.
((("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
Fiona is green.
True
1
proof
[(triple2)]
("Fiona" "is" "green" "+")
triple2
Dave is not quiet.
False
1
inv-proof
[(triple1)]
("Dave" "is" "quiet" "-")
triple1
Fiona is young.
True
2
proof
[(((triple2) -> rule3) OR ((triple2) -> rule4))]
("Fiona" "is" "young" "+")
((triple2) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
((triple2) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is not young.
False
2
inv-proof
[(((triple2) -> rule3) OR ((triple2) -> rule4))]
("Fiona" "is" "young" "-")
((triple2) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
((triple2) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is big.
True
3
proof
[(((((triple2) -> rule3)) -> rule2) OR ((((triple2) -> rule4)) -> rule2))]
("Fiona" "is" "big" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is not big.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule2) OR ((((triple2) -> rule4)) -> rule2))]
("Fiona" "is" "big" "-")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is not smart.
Unknown
inv-rconc
[@1: Fiona is smart.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Fiona" "is" "smart" "-")
Fiona is nice.
Unknown
rconc
[@2: Fiona is nice.[CWA. Example of deepest failure = (rule8 <- rule7 <- FAIL)]]
("Fiona" "is" "nice" "+")
Dave is not nice.
Unknown
inv-rconc
[@2: Dave is nice.[CWA. Example of deepest failure = (rule8 <- rule7 <- FAIL)]]
("Dave" "is" "nice" "-")
Fiona is cold.
Unknown
random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "+")
@0: Dave is quiet.[(triple1)] Fiona is green.[(triple2)] @1: Fiona is young.[(((triple2) -> rule3) OR ((triple2) -> rule4))] @2: Fiona is big.[(((((triple2) -> rule3)) -> rule2) OR ((((triple2) -> rule4)) -> rule2))]
Dave is quiet.
("Dave" "is" "quiet" "+")
triple1
Fiona is green.
("Fiona" "is" "green" "+")
triple2
Fiona is young.
("Fiona" "is" "young" "+")
((triple2) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
((triple2) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2